Lemma modulehombinop_ismodulefun {R : ring} {M N : module R} (f g : R-mod(M, N)) : @ismodulefun R M N (λ x : pr1 M, (pr1 f x * pr1 g x)%multmonoid). Proof. use make_ismodulefun. - exact (pr1 (abmonoidshombinop_ismonoidfun (modulefun_to_monoidfun f) (modulefun_to_monoidfun g))). - intros r m. rewrite (modulefun_to_islinear f). rewrite (modulefun_to_islinear g). rewrite <- module_mult_is_ldistr. reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.