Definition make_ismodulefun {R : ring} {M N : module R} {f : M -> N} (H1 : isbinopfun f) (H2 : islinear f) : ismodulefun f := tpair _ H1 H2.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.