:: deftheorem Def3 defines -th_roots_of_1 UNIROOTS:def 3 :
for n being non zero Element of NAT
for b₂ being strict Group holds
( b₂ = n -th_roots_of_1 iff ( the carrier of b₂ = n -roots_of_1 & the multF of b₂ = the multF of F_Complex || (n -roots_of_1) ) );