proposition: Lemma solvable_ext_aimg (F0 : fieldType) (L L' : splittingFieldType F0) (iota : 'AHom(L, L')) (E F : {subfield L}) : solvable_ext (iota @: E) (iota @: F) = solvable_ext E F.
proof: Proof. rewrite /solvable_ext separable_aimg; have [sepEF|]//= := boolP (separable _ _). by rewrite -aimg_normalClosure// -img_map_gal injm_sol ?map_gal_inj ?subsetT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)