proposition: Lemma map_ahom_kEnd_img s : map_ahom s \in kAEnd 1 (iota @: {: L})%AS.
proof: Proof. rewrite inE -(aimg1 iota) map_ahom_kAut// kAutfE. exact/kHom_lrmorphism/ahom_is_multiplicative. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)