{R : Ring} {M N L : LeftModule R} : LeftModuleHomomorphism N L -> LeftModuleHomomorphism M N -> LeftModuleHomomorphism M L. Proof. intros f g. snrapply Build_LeftModuleHomomorphism. - exact (grp_homo_compose f g). - intros r m. rhs_V nrapply lm_homo_lact. apply (ap f). apply lm_homo_lact. 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.