proposition: Lemma kHom_is_multiplicative : kHom K E f -> multiplicative kHomf.
proof: Proof. case/kHomP=> fM idKf; rewrite /kHomf. by split=> [a b|] /=; [rewrite /= fM ?subvsP | rewrite algid1 idKf // mem1v]. 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)