:: deftheorem defines divides HURWITZ:def 7 :
for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, s being Polynomial of L holds
( s divides p iff p mod s = 0_. L );