proposition: Lemma inv_map_ahom_in (f : 'End(L')) (E : {subfield L}) : (f @: (iota @: E) <= limg iota)%VS -> ahom_in E (inv_map_hom iota f) = ahom_in (iota @: E) f.
proof: Proof. by move=> fiotaE; rewrite -!k1HomE inv_map_hom_kHom ?sub1v// aimg1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)