{R : Ring} {M N : RightModule R} (f : M $-> N) : RightSubmodule M := lm_kernel (R:=rng_op R) f. Global Instance isleftsubmodule_grp_image {R : Ring} {M N : LeftModule R} (f : M $-> N) : IsLeftSubmodule (grp_image f). Proof. srapply Build_IsLeftSubmodule. intros r m; apply Trunc_functor; intros [n p]. exists (r *L n). lhs nrapply lm_homo_lact. apply ap. exact p. 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.