proposition: Lemma limg_inv_map_ahom (E : {subfield L}) (f : 'End(L')) : ((f @: (iota @: E)) <= (iota @: E))%VS -> (iota @: (inv_map_hom iota f @: E))%VS = (f @: (iota @: E))%VS.
proof: Proof. move=> fiotaE; rewrite -!limg_comp; apply/vspaceP => x. have fiota u : u \in E -> f (iota u) \in limg iota. move=> uE; rewrite memvE (@subv_trans _ _ (f @: (iota @: E))%VS) //. by rewrite -memvE !(memv_img, limgS). by rewrite (subv_trans fiotaE) ?limgS ?subvf. by apply/memv_imgP/memv_imgP => -[u uE ->]; exists u => //; rewrite [LHS]comp_lfunE [RHS]comp_lfunE inv_map_homE// ?fiota. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)