:: deftheorem defines mod HURWITZ:def 6 :
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 p mod s = p - ((p div s) *' s);