proposition: Lemma solvable_by_radical_polyP (F : fieldType) (p : {poly F}) : p != 0 -> has_char0 F -> solvable_by_radical_poly p <-> classically (exists (L : splittingFieldType F) (rs : seq L), p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) /\ solvable_by radical 1 <<1 & rs>>).
proof: Proof. move=> p_neq0 charF0; split => sol_p; last first. apply/AbelGaloisPoly => //; apply/solvable_ext_polyP => //. apply: classic_bind sol_p => -[L [rs [prs sol_p]]]; apply/classicW. exists L, rs; split => //; rewrite -galois_solvable. apply: radical_ext_solvable_ext; rewrite ?sub1v// => v. by rewrite char_lalg charF0. have charL : has_char0 L by move=> n; rewrite char_lalg charF0. rewrite char0_galois// ?sub1v//. apply/splitting_normalField; rewrite ?sub1v//. by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs]. have FoE (v : F^o) : v = in_alg F^o v by rewrite /= /(_%:A)/= mulr1. apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0). move=> [L [rs [f rsf p_eq]]]. have fF : f =1 in_alg L by move=> v; rewrite [v in LHS]FoE rmorph_alg. have splitL : SplittingField.axiom L. exists (p ^^ f); first by apply/polyOver1P; exists p; apply: eq_map_poly. exists rs => //; suff <- : limg f = 1%VS by []. apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v. by move=> /memv_imgP[u _ ->]; rewrite fF/= rpredZ// rpred1. pose sM := FieldExt_isSplittingField.Build F L splitL. pose S : splittingFieldType F := HB.pack L sM. pose d := \dim <<1 & (rs : seq S)>>. have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F. by have /charf0P-> := charF0; rewrite -lt0n adim_gt0. apply/classic_bind => -[C [w [g wg w_prim]]]; apply/classicW. have gf : g \o f =1 in_alg C by move=> v /=; rewrite fF rmorph_alg. have pgrs : p ^^ in_alg C %= \prod_(x <- [seq g i | i <- rs]) ('X - x%:P). by rewrite -(eq_map_poly gf) map_poly_comp/= -map_prod_XsubC eqp_map//. exists C, (map g rs); split => //=; apply: (sol_p C (map g rs) _ w) => //. by rewrite -(aimg1 g) -aimg_adjoin_seq dim_aimg. 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)