proposition: Lemma AbelGaloisPoly (F : fieldType) (p : {poly F}) : has_char0 F -> solvable_ext_poly p <-> solvable_by_radical_poly p.
proof: Proof. move=> charF; split=> + L rs pE => [/(_ L rs pE) + w w_prim|solrs]/=. have charL : has_char0 L by move=> i; rewrite char_lalg. have normal_rs : normalField 1 <<1 & rs>>. apply/splitting_normalField; rewrite ?sub1v//. by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs]. by move=> solrs; apply/(@AbelGalois _ _ w); rewrite ?char0_solvable_extE ?normalClosure_id ?sub1v ?dimv1 ?divn1. have charL : has_char0 L by move=> i; rewrite char_lalg. have seprs: separable 1 <<1 & rs>> by apply/char0_separable. have normal_rs : normalField 1 <<1 & rs>>. apply/splitting_normalField; rewrite ?sub1v//. by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs]. pose n := \dim <<1 & rs>>. have nFN0 : n%:R != 0 :> F by have /charf0P-> := charF; rewrite -lt0n adim_gt0. apply: (@classic_cycloSplitting _ L _ nFN0) => - [L' [w [iota wL' w_prim]]]. suff: solvable_ext 1 <<1 & rs>>. by rewrite /solvable_ext seprs normalClosure_id ?sub1v. rewrite -(solvable_ext_aimg iota). have charL' : [char L'] =i pred0 by move=> i; rewrite char_lalg. apply/(@AbelGalois _ _ w) => //. - by rewrite limgS// sub1v. - rewrite -aimg_normalClosure //= aimg1 dimv1 divn1 dim_aimg/=. by rewrite normalClosure_id ?dimv1 ?divn1 ?sub1v//. have /= := solrs L' (map iota rs) _ w. rewrite -(aimg1 iota) -!aimg_adjoin_seq dim_aimg. apply => //; have := pE; rewrite -(eqp_map iota). by rewrite -map_poly_comp/= (eq_map_poly (rmorph_alg _)) map_prod_XsubC. 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)