Build_RightModuleHomomorphism' {R :Ring} {M N : RightModule R} (f : M -> N) (p : forall r x y, f (x *R r + y) = f x *R r + f y) : RightModuleHomomorphism M N := Build_LeftModuleHomomorphism' (R:=rng_op R) f p.
Require Import WildCat. Require Import Spaces.Nat.Core. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring.