Lemma modulehomabgr_isabgrop {R : ring} (M N : module R) : isabgrop (λ f g : R-mod(M, N), modulehombinop f g). Proof. use make_isabgrop. use make_isgrop. - use modulehomabmodule_ismoduleop. - use make_invstruct. + intros f. exact (modulehombinop_inv f). + use make_isinv. * intros f. exact (modulehombinop_linvax f). * intros f. exact (modulehombinop_rinvax f). - intros f g. exact (modulehombinop_comm f g). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.