proposition: Lemma map_ahomE (f : 'AEnd(L)) x : map_ahom f (iota x) = iota (f x).
proof: Proof. by rewrite -!comp_lfunE map_ahomC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)