proposition: Lemma inv_kHomf K f : kHom K {:L} f -> kHom K {:L} f^-1.
proof: Proof. move=> homKf; have [[fM idKf] kerf0] := (kHomP homKf, kAutf_lker0 homKf). have f1K: cancel f^-1%VF f by apply: lker0_lfunVK. apply/kHomP; split=> [x y _ _ | x Kx]; apply: (lker0P kerf0). by rewrite fM ?memvf ?{1}f1K. by rewrite f1K idKf. 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)