proposition: Lemma solvableWradical_ext w E F (n := \dim_E F) : n.-primitive_root w -> w \in E -> galois E F -> solvable 'Gal(F / E) -> radical.-ext E F.
proof: Proof. move=> + + galEF; have [k] := ubnP n; elim: k => // k IHk in w E F n galEF *. rewrite ltnS => le_nk; have subEF : (E <= F)%VS by case/andP: galEF. have n_gt0 : (0 < n)%N by rewrite ltn_divRL ?field_dimS// mul0n adim_gt0. move=> wn Ew solEF; have [n_le1|n_gt1] := leqP n 1%N. have /eqP : n = 1%N by case: {+}n n_gt0 n_le1 => [|[]]. rewrite -eqn_mul ?adim_gt0 ?field_dimS// mul1n eq_sym dimv_leqif_eq//. by rewrite val_eqE => /eqP<-; apply: rext_refl. have /sol_prime_factor_exists[|H Hnormal] := solEF. by rewrite -cardG_gt1 -galois_dim. have [<-|H_neq] := eqVneq H ('Gal(F / E))%G; first by rewrite indexgg. have galEH := normal_fixedField_galois galEF Hnormal. have subEH : (E <= fixedField H)%VS by case/andP: galEH. rewrite -dim_fixed_galois ?normal_sub// galois_dim//=. pose d := \dim_E (fixedField H); pose p := \dim_(fixedField H) F. have p_gt0 : (p > 0)%N by rewrite divn_gt0 ?adim_gt0 ?dimvS ?fixedField_bound. have n_eq : n = (p * d)%N by rewrite /p /d -dim_fixedField dim_fixed_galois; rewrite ?Lagrange ?normal_sub -?galois_dim. have Ewm : w ^+ (n %/ d) \in E by rewrite rpredX. move=> /prime_cyclic/cyclic_radical_ext-/(_ _ _ Ewm galEH)/=. rewrite dvdn_prim_root// => [/(_ isT)|]; last by rewrite n_eq dvdn_mull. move=> /rext_trans; apply; apply: (IHk (w ^+ (n %/ p))) => /=. - exact: fixedField_galois. - rewrite (leq_trans _ le_nk)// -dim_fixedField /n galois_dim// proper_card//. by rewrite properEneq H_neq normal_sub. - by rewrite dvdn_prim_root// n_eq dvdn_mulr. - by rewrite rpredX//; apply: subvP Ew. - by rewrite gal_fixedField (solvableS (normal_sub Hnormal)). 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)