theorem Th41: :: NUMBER19:41

for R being Field
for p being Polynomial of R
for a being Element of R st a is_a_root_of p holds
p = (p div (rpoly (1,a))) *' (rpoly (1,a))