:: deftheorem Def5 defines div HURWITZ:def 5 :
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 st s <> 0_. L holds
for b₄ being Polynomial of L holds
( b₄ = p div s iff ex t being Polynomial of L st
( p = (b₄ *' s) + t & deg t < deg s ) );