{R : Ring} {M N : LeftModule R} (L : LeftModule R) (f : L $-> M) (g : L $-> N) : L $-> lm_prod M N. Proof. snrapply Build_LeftModuleHomomorphism. - apply (grp_prod_corec f g). - intros r l. apply path_prod; 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.