proposition: Lemma modulehomabgr_isabgrop {R : ring} (M N : module R) : isabgrop (λ f g : R-mod(M, N), modulehombinop f g).
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids