theorem :: UNIROOTS:37
for n being non zero Element of NAT holds n -th_roots_of_1 is Subgroup of MultGroup F_Complex