proposition: Lemma map_ahomC (f : 'AEnd(L)) : (map_ahom f \o iota)%VF = (iota \o f)%VF.
proof: Proof. by rewrite /map_ahom; case: map_ahom_subproof. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)