proposition: Lemma kHomP {K V f} : reflect [/\ {in V &, forall x y, f (x * y) = f x * f y} & {in K, forall x, f x = x}] (kHom K V f).
proof: Proof. apply: (iffP andP) => [[/ahom_inP[fM _] /subvP idKf] | [fM idKf]]. by split=> // x /idKf/fixedSpaceP. split; last by apply/subvP=> x /idKf/fixedSpaceP. by apply/ahom_inP; split=> //; rewrite 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)