proposition: Lemma map_ahom_in (f : 'End(L)) (E : {vspace L}) : ahom_in (iota @: E) (map_hom iota f) = ahom_in E f.
proof: Proof. apply/ahom_inP/ahom_inP => -[mfM mf1]; last first. split; last by rewrite -(rmorph1 iota) map_hom_algE mf1. move=> _ _ /memv_imgP[u uE ->] /memv_imgP[v vE ->]. by rewrite !(map_hom_algE, =^~rmorphM)/= mfM. split=> [x y xE yE|]; last first. have : map_hom iota f (iota 1) = iota 1 by rewrite rmorph1. by rewrite map_hom_algE => /fmorph_inj. have := mfM _ _ (memv_img iota xE) (memv_img iota yE). by rewrite !(map_hom_algE, =^~rmorphM)/= => /fmorph_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)