proposition: Lemma map_ahom_subproof (f : 'AEnd(L)) : {g : 'AEnd(L') | (g \o iota)%VF = (iota \o f)%VF }.
proof: Proof. have : kHom 1%VS (iota @: {: L})%VS (map_hom iota f). by rewrite k1HomE map_ahom_in ahomWin. move=> /kHom_to_AEnd[g gP]; exists g. apply/lfunP => x; rewrite !comp_lfunE/=. by rewrite -map_hom_algE gP ?memv_img// memvf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)