Definition modulehommodule {R : commring} (M N : module R) : module R. Proof. use make_module. use (modulehomabgr M N). use mult_to_module_struct. exact modulehombinop_smul. - intros r f g. use modulefun_paths2. intros x. apply module_mult_is_ldistr. - intros r r0 f. use modulefun_paths2. intros x. apply module_mult_is_rdistr. - intros r r0 f. use modulefun_paths2. intros x. apply module_mult_assoc. - intros f. use modulefun_paths2. intros x. cbn. apply module_mult_unel2. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.