theorem Th35: :: UNIROOTS:35

for n being non zero Element of NAT holds n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n }