proposition: Lemma kHom_inv K E f : kHom K E f -> {in E, {morph f : x / x^-1}}.
proof: Proof. case/kHomP=> fM idKf x Ex. have [-> | nz_x] := eqVneq x 0; first by rewrite linear0 invr0 linear0. have fxV: f x * f x^-1 = 1 by rewrite -fM ?rpredV ?divff // idKf ?mem1v. have Ufx: f x \is a GRing.unit by apply/unitrPr; exists (f x^-1). by apply: (mulrI Ufx); rewrite divrr. 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)