theorem Th42: :: UNIROOTS:42

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