{R : Ring} {M : RightModule R} : RightSubmodule M -> Subgroup M := idmap. Coercion : RightSubmodule >-> Subgroup. Global Instance isleftmodule_leftsubmodule {R : Ring} {M : LeftModule R} (N : LeftSubmodule M) : IsLeftModule R N. Proof. snrapply Build_IsLeftModule. - intros r [n n_in_N]. exists (r *L n). by apply lsm_submodule. - intros r [n] [m]; apply path_sigma_hprop. apply lact_left_dist. - intros r s [n]; apply path_sigma_hprop. apply lact_right_dist. - intros r s [n]; apply path_sigma_hprop. apply lact_assoc. - intros [n]; apply path_sigma_hprop. apply lact_unit. 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.