proposition: Lemma normal_solvable (F0 : fieldType) (L : splittingFieldType F0) (E F : {subfield L}) : has_char0 L -> (E <= F)%VS -> normalField E F -> solvable_ext E F = solvable 'Gal(F / E).
proof: Proof. by move=> charL EF /(char0_galois charL EF)/galois_solvable. 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)