theorem :: UNIROOTS:58

for n, q being non zero Element of NAT
for qc being Element of F_Complex st qc = q holds
for j being Integer st j = eval ((cyclotomic_poly n),qc) holds
j divides (q |^ n) - 1