Build_LeftModuleHomomorphism' {R : Ring} {M N : LeftModule R} (f : M -> N) (p : forall r x y, f (r *L x + y) = r *L f x + f y) : LeftModuleHomomorphism M N. Proof. snrapply Build_LeftModuleHomomorphism. - snrapply Build_GroupHomomorphism. + exact f. + intros x y. rewrite <- (lm_unit (f x)). set (lact 1 (f x)). rewrite <- (lm_unit x). apply p. - intros r m. simpl. rewrite <- (grp_unit_r (lact r m)). rewrite p. rhs_V nrapply grp_unit_r. apply grp_cancelL. specialize (p 1 0 0). rewrite 2 lm_unit in p. apply (grp_cancelL1 (z := f 0)). lhs_V nrapply p. apply ap. apply grp_unit_l. Defined.
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.