proposition: Lemma kAutf_lker0 K f : kHom K {:L} f -> lker f == 0%VS.
proof: Proof. move/(kHomSl (sub1v _))/kHom_lrmorphism=> fM. pose fmM := GRing.isMultiplicative.Build _ _ _ fM. pose fRM : GRing.RMorphism.type _ _ := HB.pack (fun_of_lfun f) fmM. by apply/lker0P; apply: (fmorph_inj fRM). 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)