proposition: Theorem AbelGaloisPolyRat (p : {poly rat}) : reflect (solvable_by_radical_poly p) (solvable 'Gal({: numfield p} / 1)).
proof: Proof. have [{p}->|p_neq0] := eqVneq p 0. rewrite numfield0 regular_fullv galvv solvable1; constructor. move=> L rs; rewrite eqp_sym rmorph0 eqp0 prodf_seq_eq0. by move=> /hasP[x _ /=]; rewrite polyXsubC_eq0. have charrat : [char rat] =i pred0 by exact: char_num. pose charnumfield := char_ext (numfield p). apply: (equivP idP); rewrite -AbelGaloisPoly//. have [rs prs <-] := numfieldP p_neq0. split; last by move=> /(_ (numfield p) rs prs). move=> solp; apply/solvable_ext_polyP => //. by apply/classicW; exists (numfield p); exists rs; split. 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)