proposition: Lemma cyclotomic_over : cyclotomic w n \is a polyOver E.
proof: Proof. by apply/polyOverP=> i; rewrite -Phi_cyclotomic // coef_map /= rpred_int. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)