Definition carrierofasubmodule {R : ring} {M : module R} (A : submodule M) : module R. Proof. use mult_to_module. - exact (carrierofasubabgr A). - exact (submodule_smul). - intros r a b. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_is_ldistr. - intros r s a. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_is_rdistr. - intros r s a. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_assoc. - intros f. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_unel2. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Modules.Core.