proposition: Lemma kHom_to_AEnd K E f : kHom K E f -> {g : 'AEnd(L) | {in E, f =1 val g}}.
proof: Proof. move=> homKf; have{homKf} [homFf sFE] := (kHomSl (sub1v K) homKf, sub1v E). have [p Fp /(splittingFieldForS sFE (subvf E))splitLp] := splittingPoly. have [g0 homLg0 eq_fg] := kHom_extends sFE homFf Fp splitLp. by apply: exist (Sub g0 _) _ => //; apply/ahomP/kHom_lrmorphism. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)