proposition: Lemma galois_solvable_by_radical w E F (n := \dim_E F) : n.-primitive_root w -> galois E F -> solvable 'Gal(F / E) -> solvable_by radical E F.
proof: Proof. move=> w_root galEF solEF; have [EF Ew] := (galois_subW galEF, subv_adjoin E w). exists (F * <<E; w>>)%AS; last by rewrite field_subvMr. apply: rext_trans (radicalext_Fadjoin_cyclotomic _ w_root) _. have galEwFEw: galois <<E; w>> (F * <<E; w>>) by apply: galois_prodvr galEF. pose m := \dim_<<E; w>> (F * <<E; w>>); pose w' := w ^+ (n %/ m). have w'Ew : w' \in <<E; w>>%VS by rewrite rpredX ?memv_adjoin. have w'prim : m.-primitive_root w'. rewrite dvdn_prim_root // /m /n !galois_dim//. by rewrite (card_isog (galois_isog galEF _)) ?cardSg ?galS ?subv_cap ?EF//. apply: (@solvableWradical_ext w'); rewrite // (isog_sol (galois_isog galEF _))//. by rewrite (solvableS _ solEF) ?galS// subv_cap EF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)