theorem :: UNIROOTS:37

for n being non zero Element of NAT holds n -th_roots_of_1 is Subgroup of MultGroup F_Complex