:: deftheorem defines -roots_of_1 UNIROOTS:def 2 :
for n being non zero Element of NAT holds n -roots_of_1 = { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ;