{R : Ring} (M N : LeftModule R) := { lm_homo_map :> GroupHomomorphism M N; lm_homo_lact : forall r m, lm_homo_map (r *L m) = r *L lm_homo_map m; }.
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.