Lemma modulehombinop_inv_ismodulefun {R : ring} {M N : module R} (f : R-mod(M, N)) : ismodulefun (λ m : M, grinv N (pr1 f m)). Proof. use tpair. - use make_isbinopfun. intros x x'. cbn. rewrite (pr1 (pr2 f)). rewrite (pr2 (pr2 (pr1module N))). use (grinvop N). - intros r m. rewrite <- module_inv_mult. apply maponpaths. apply (pr2 f). Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.