proposition: Lemma map_ahom_kAEnd s (E F : {subfield L}) : (map_ahom s \in kAEnd (iota @: E)%VS (iota @: F)%VS) = (s \in kAEnd E F).
proof: Proof. by rewrite !inE map_ahom_kAut. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)