proposition: Lemma abelian_cyclotomic : abelian 'Gal(<<E; w>> / E)%g.
proof: Proof. case: (boolP (w \in E)) => [w_in_E |w_notin_E]. suff -> : ('Gal(<<E; w>> / E) = 1)%g by apply: abelian1. apply/eqP; rewrite -subG1; apply/subsetP => x x_in. rewrite inE gal_adjoin_eq ?group1 // (fixed_gal _ x_in w_in_E) ?gal_id //. by have /Fadjoin_idP H := w_in_E; rewrite -{1}H subvv. rewrite card_classes_abelian /classes. apply/eqP; apply: card_in_imset => f g f_in g_in; rewrite -!orbitJ. move/orbit_eqP/orbitP => [] h h_in <- {f f_in}; apply/eqP. rewrite gal_adjoin_eq //= /conjg /= ?groupM ?groupV //. rewrite ?galM ?memv_gal ?memv_adjoin //. have hg_gal f : f \in 'Gal(<<E; w>> / E)%g -> f w ^+ n = 1. by move=> f_in; apply/prim_expr_order; rewrite fmorph_primitive_root. have := svalP (prim_rootP w_is_nth_root (hg_gal _ g_in)). have h1_in : (h ^-1)%g \in 'Gal(<<E; w>> / E)%g by rewrite ?groupV. have := svalP (prim_rootP w_is_nth_root (hg_gal _ h1_in)). set ih1 := sval _ => hh1; set ig := sval _ => hg. rewrite hh1 rmorphX /= hg exprAC -hh1 rmorphX /=. by rewrite -galM ?memv_adjoin // mulVg gal_id. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)