theorem Th46: :: UNIROOTS:46

for n being non zero Element of NAT holds unital_poly (F_Complex,n) = poly_with_roots (((n -roots_of_1),1) -bag)