proposition: Lemma galois_Fadjoin_cyclotomic : galois E <<E; w>>.
proof: Proof. apply/splitting_galoisField; exists (cyclotomic w n). split; rewrite ?cyclotomic_over//; last exact: splitting_Fadjoin_cyclotomic. rewrite /cyclotomic -(big_image _ _ _ _ (fun x => 'X - x%:P))/=. rewrite separable_prod_XsubC map_inj_uniq ?enum_uniq// => i j /eqP. by rewrite (eq_prim_root_expr w_is_nth_root) !modn_small// => /eqP/val_inj. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)