theorem Th47: :: UPROOTS:50

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
p = <%(- r),(1. L)%> *' (poly_quotient (p,r))