proposition: Lemma AbelGalois (F0 : fieldType) (L : splittingFieldType F0) (w : L) (E F : {subfield L}) : (E <= F)%VS -> has_char0 L -> (\dim_E (normalClosure E F)).-primitive_root w -> solvable_by radical E F <-> solvable_ext E F.
proof: Proof. move=> EF charL wprim; split; first exact: radical_ext_solvable_ext. exact: (ext_solvable_by_radical wprim). 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)