for n, ni, q being non zero Element of NAT st ni < n & ni divides n holds
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) div ((q |^ ni) - 1)