:: deftheorem Def6 defines poly_quotient UPROOTS:def 7 :
for L being non degenerated comRing
for r being Element of L
for p being Polynomial of L st r is_a_root_of p holds
for b₄ being Polynomial of L holds
( ( len p > 0 implies ( b₄ = poly_quotient (p,r) iff ( (len b₄) + 1 = len p & ( for i being Nat holds b₄ . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) ) & ( not len p > 0 implies ( b₄ = poly_quotient (p,r) iff b₄ = 0_. L ) ) );