proposition: Lemma pradical_solvable_ext (p : nat) (F0 : fieldType) (L : splittingFieldType F0) (E : {subfield L}) (x : L) : prime p -> p%:R != 0 :> F0 -> x ^+ p \in E -> solvable_ext E <<E; x>>.
proof: Proof. move=> p_prime p_neq0 xpE; have p_gt0 := prime_gt0 p_prime. wlog [w w_root] : L E x xpE / {w : L | p.-primitive_root w} => [hwlog|]. apply: (@classic_cycloSplitting _ L p p_neq0) => -[L' [w [f wf rw]]]. rewrite -(solvable_ext_aimg f) aimg_adjoin hwlog -?rmorphX ?memv_img//. by exists w. have galEw := galois_Fadjoin_cyclotomic E w_root. have solEw := solvable_Fadjoin_cyclotomic E w_root. have [xEw|xNEw] := boolP (x \in <<E; w>>%VS). by apply/solvable_extP; exists <<E; w>>%AS; rewrite galEw solEw Fadjoin_sub. have xpEw : x ^+ p \in <<E; w>>%VS by rewrite (subvP (subv_adjoin _ _)). have galEwx : galois E <<<<E; w>>; x>> by rewrite (@galois_cyclo_radical p). apply/solvable_extP; exists <<<<E; x>>; w>>%AS; rewrite subv_adjoin/= adjoinC. rewrite galEwx (@series_sol _ _ ('Gal(<<<<E; w>>; x>> / <<E; w>>))); last by rewrite normalField_normal ?subv_adjoin ?galois_normalW. rewrite (@pradical_solvable p _ _ w)// ?memv_adjoin//. by rewrite (isog_sol (normalField_isog _ _ _)) ?galois_normalW ?subv_adjoin. 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)