Documentation

Mathlib.Algebra.Module.Submodule.Basic

Submodules of a module #

In this file we define

Tags #

submodule, subspace, linear map

class SubmoduleClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [inst : AddZeroClass M] [inst : SMul R M] [inst : SetLike S M] [inst : AddSubmonoidClass S M] extends SMulMemClass :

    SubmoduleClass S R M says S is a type of submodules s ≤ M.

    Note that only R is marked as outParam since M is already supplied by the SetLike class.

    Instances
      structure Submodule (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] extends AddSubmonoid :
      • The carrier set is closed under scalar multiplication.

        smul_mem' : ∀ (c : R) {x : M}, x toAddSubmonoid.toAddSubsemigroup.carrierc x toAddSubmonoid.toAddSubsemigroup.carrier

      A submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.

      Instances For
        abbrev Submodule.toSubMulAction {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (self : Submodule R M) :

        Reinterpret a Submodule as an SubMulAction.

        Equations
        • One or more equations did not get rendered due to their size.
        instance Submodule.setLike {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        Equations
        • One or more equations did not get rendered due to their size.
        instance Submodule.submoduleClass {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        Equations
        • Submodule.submoduleClass = SubmoduleClass.mk
        @[simp]
        theorem Submodule.mem_toAddSubmonoid {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) (x : M) :
        x p.toAddSubmonoid x p
        @[simp]
        theorem Submodule.mem_mk {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : AddSubmonoid M} {x : M} (h : ∀ (c : R) {x : M}, x S.toAddSubsemigroup.carrierc x S.toAddSubsemigroup.carrier) :
        x { toAddSubmonoid := S, smul_mem' := h } x S
        @[simp]
        theorem Submodule.coe_set_mk {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (S : AddSubmonoid M) (h : ∀ (c : R) {x : M}, x S.toAddSubsemigroup.carrierc x S.toAddSubsemigroup.carrier) :
        { toAddSubmonoid := S, smul_mem' := h } = S
        @[simp]
        theorem Submodule.mk_le_mk {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : AddSubmonoid M} {S' : AddSubmonoid M} (h : ∀ (c : R) {x : M}, x S.toAddSubsemigroup.carrierc x S.toAddSubsemigroup.carrier) (h' : ∀ (c : R) {x : M}, x S'.toAddSubsemigroup.carrierc x S'.toAddSubsemigroup.carrier) :
        { toAddSubmonoid := S, smul_mem' := h } { toAddSubmonoid := S', smul_mem' := h' } S S'
        theorem Submodule.ext {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} (h : ∀ (x : M), x p x q) :
        p = q
        @[simp]
        theorem Submodule.carrier_inj {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} :
        p.toAddSubmonoid.toAddSubsemigroup.carrier = q.toAddSubmonoid.toAddSubsemigroup.carrier p = q
        def Submodule.copy {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) (s : Set M) (hs : s = p) :

        Copy of a submodule with a new carrier equal to the old one. Useful to fix definitional equalities.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Submodule.coe_copy {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (S : Submodule R M) (s : Set M) (hs : s = S) :
        ↑(Submodule.copy S s hs) = s
        theorem Submodule.copy_eq {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (S : Submodule R M) (s : Set M) (hs : s = S) :
        Submodule.copy S s hs = S
        theorem Submodule.toAddSubmonoid_injective {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        Function.Injective Submodule.toAddSubmonoid
        @[simp]
        theorem Submodule.toAddSubmonoid_eq {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} :
        p.toAddSubmonoid = q.toAddSubmonoid p = q
        theorem Submodule.toAddSubmonoid_strictMono {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        StrictMono Submodule.toAddSubmonoid
        theorem Submodule.toAddSubmonoid_le {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} :
        p.toAddSubmonoid q.toAddSubmonoid p q
        theorem Submodule.toAddSubmonoid_mono {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        Monotone Submodule.toAddSubmonoid
        @[simp]
        theorem Submodule.coe_toAddSubmonoid {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) :
        p.toAddSubmonoid = p
        theorem Submodule.toSubMulAction_injective {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        Function.Injective Submodule.toSubMulAction
        theorem Submodule.toSubMulAction_eq {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} :
        theorem Submodule.toSubMulAction_strictMono {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        StrictMono Submodule.toSubMulAction
        theorem Submodule.toSubMulAction_mono {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        Monotone Submodule.toSubMulAction
        @[simp]
        theorem Submodule.coe_toSubMulAction {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) :
        instance SubmoduleClass.toModule {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {A : Type u_1} [inst : SetLike A M] [inst : AddSubmonoidClass A M] [inst : SubmoduleClass A R M] (S' : A) :
        Module R { x // x S' }

        A submodule of a Module is a Module.

        Equations
        def SubmoduleClass.subtype {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {A : Type u_1} [inst : SetLike A M] [inst : AddSubmonoidClass A M] [inst : SubmoduleClass A R M] (S' : A) :
        { x // x S' } →ₗ[R] M

        The natural R-linear map from a submodule of an R-module M to M.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem SubmoduleClass.coeSubtype {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {A : Type u_1} [inst : SetLike A M] [inst : AddSubmonoidClass A M] [inst : SubmoduleClass A R M] (S' : A) :
        ↑(SubmoduleClass.subtype S') = Subtype.val
        theorem Submodule.mem_carrier {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} :
        x p.toAddSubmonoid.toAddSubsemigroup.carrier x p
        @[simp]
        theorem Submodule.zero_mem {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        0 p
        theorem Submodule.add_mem {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (h₁ : x p) (h₂ : y p) :
        x + y p
        theorem Submodule.smul_mem {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} (r : R) (h : x p) :
        r x p
        theorem Submodule.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] (r : S) (h : x p) :
        r x p
        theorem Submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ιM} :
        (∀ (c : ι), c tf c p) → (Finset.sum t fun i => f i) p
        theorem Submodule.sum_smul_mem {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ιM} (r : ιR) (hyp : ∀ (c : ι), c tf c p) :
        (Finset.sum t fun i => r i f i) p
        @[simp]
        theorem Submodule.smul_mem_iff' {G : Type u''} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [inst : Group G] [inst : MulAction G M] [inst : SMul G R] [inst : IsScalarTower G R M] (g : G) :
        g x p x p
        instance Submodule.add {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        Add { x // x p }
        Equations
        • Submodule.add p = { add := fun x y => { val := x + y, property := (_ : x + y p) } }
        instance Submodule.zero {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        Zero { x // x p }
        Equations
        instance Submodule.inhabited {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        Inhabited { x // x p }
        Equations
        instance Submodule.smul {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] :
        SMul S { x // x p }
        Equations
        instance Submodule.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] :
        IsScalarTower S R { x // x p }
        Equations
        instance Submodule.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {S' : Type u_1} [inst : SMul S R] [inst : SMul S M] [inst : SMul S' R] [inst : SMul S' M] [inst : SMul S S'] [inst : IsScalarTower S' R M] [inst : IsScalarTower S S' M] [inst : IsScalarTower S R M] :
        IsScalarTower S S' { x // x p }
        Equations
        instance Submodule.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] [inst : SMul Sᵐᵒᵖ R] [inst : SMul Sᵐᵒᵖ M] [inst : IsScalarTower Sᵐᵒᵖ R M] [inst : IsCentralScalar S M] :
        IsCentralScalar S { x // x p }
        Equations
        theorem Submodule.nonempty {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        @[simp]
        theorem Submodule.mk_eq_zero {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} (h : x p) :
        { val := x, property := h } = 0 x = 0
        theorem Submodule.coe_eq_zero {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {x : { x // x p }} :
        x = 0 x = 0
        @[simp]
        theorem Submodule.coe_add {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : { x // x p }) (y : { x // x p }) :
        ↑(x + y) = x + y
        @[simp]
        theorem Submodule.coe_zero {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} :
        0 = 0
        theorem Submodule.coe_smul {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (r : R) (x : { x // x p }) :
        ↑(r x) = r x
        @[simp]
        theorem Submodule.coe_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] (r : S) (x : { x // x p }) :
        ↑(r x) = r x
        theorem Submodule.coe_mk {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : M) (hx : x p) :
        { val := x, property := hx } = x
        theorem Submodule.coe_mem {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : { x // x p }) :
        x p
        instance Submodule.addCommMonoid {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        AddCommMonoid { x // x p }
        Equations
        instance Submodule.module' {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [inst : Semiring S] [inst : SMul S R] [inst : Module S M] [inst : IsScalarTower S R M] :
        Module S { x // x p }
        Equations
        • One or more equations did not get rendered due to their size.
        instance Submodule.module {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        Module R { x // x p }
        Equations
        def Submodule.subtype {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        { x // x p } →ₗ[R] M

        Embedding of a submodule p to the ambient space M.

        Equations
        • One or more equations did not get rendered due to their size.
        theorem Submodule.subtype_apply {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (x : { x // x p }) :
        ↑(Submodule.subtype p) x = x
        @[simp]
        theorem Submodule.coeSubtype {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        ↑(Submodule.subtype p) = Subtype.val
        theorem Submodule.injective_subtype {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        theorem Submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (x : ι{ x // x p }) (s : Finset ι) :
        ↑(Finset.sum s fun i => x i) = Finset.sum s fun i => ↑(x i)

        Note the AddSubmonoid version of this lemma is called AddSubmonoid.coe_finset_sum.

        def Submodule.restrictScalars (S : Type u') {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (V : Submodule R M) :

        V.restrict_scalars S is the S-submodule of the S-module given by restriction of scalars, corresponding to V, an R-submodule of the original R-module.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Submodule.coe_restrictScalars (S : Type u') {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (V : Submodule R M) :
        @[simp]
        theorem Submodule.restrictScalars_mem (S : Type u') {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (V : Submodule R M) (m : M) :
        @[simp]
        theorem Submodule.restrictScalars_self {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (V : Submodule R M) :
        theorem Submodule.restrictScalars_injective (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] :
        @[simp]
        theorem Submodule.restrictScalars_inj (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] {V₁ : Submodule R M} {V₂ : Submodule R M} :
        instance Submodule.restrictScalars.origModule (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (p : Submodule R M) :

        Even though p.restrictScalars S has type Submodule S M, it is still an R-module.

        Equations
        instance Submodule.restrictScalars.isScalarTower (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (p : Submodule R M) :
        Equations
        @[simp]
        theorem Submodule.restrictScalarsEmbedding_apply (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (V : Submodule R M) :
        def Submodule.restrictScalarsEmbedding (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] :

        restrictScalars S is an embedding of the lattice of R-submodules into the lattice of S-submodules.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Submodule.restrictScalarsEquiv_apply (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (p : Submodule R M) (a : { x // x Submodule.restrictScalars S p }) :
        @[simp]
        theorem Submodule.restrictScalarsEquiv_symm_apply (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (p : Submodule R M) (a : { x // x p }) :
        def Submodule.restrictScalarsEquiv (S : Type u') (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Semiring S] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : IsScalarTower S R M] (p : Submodule R M) :
        { x // x Submodule.restrictScalars S p } ≃ₗ[R] { x // x p }

        Turning p : Submodule R M into an S-submodule gives the same module structure as turning it into a type and adding a module structure.

        Equations
        • One or more equations did not get rendered due to their size.
        theorem Submodule.neg_mem {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} (hx : x p) :
        -x p
        def Submodule.toAddSubgroup {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

        Reinterpret a submodule as an additive subgroup.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Submodule.coe_toAddSubgroup {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
        @[simp]
        theorem Submodule.mem_toAddSubgroup {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} :
        theorem Submodule.toAddSubgroup_injective {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} :
        Function.Injective Submodule.toAddSubgroup
        @[simp]
        theorem Submodule.toAddSubgroup_eq {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (p' : Submodule R M) :
        theorem Submodule.toAddSubgroup_strictMono {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} :
        StrictMono Submodule.toAddSubgroup
        theorem Submodule.toAddSubgroup_le {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (p' : Submodule R M) :
        theorem Submodule.toAddSubgroup_mono {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} :
        Monotone Submodule.toAddSubgroup
        theorem Submodule.sub_mem {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :
        x py px - y p
        theorem Submodule.neg_mem_iff {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} :
        -x p x p
        theorem Submodule.add_mem_iff_left {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :
        y p → (x + y p x p)
        theorem Submodule.add_mem_iff_right {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :
        x p → (x + y p y p)
        theorem Submodule.coe_neg {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (x : { x // x p }) :
        ↑(-x) = -x
        theorem Submodule.coe_sub {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (x : { x // x p }) (y : { x // x p }) :
        ↑(x - y) = x - y
        theorem Submodule.sub_mem_iff_left {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (hy : y p) :
        x - y p x p
        theorem Submodule.sub_mem_iff_right {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (hx : x p) :
        x - y p y p
        instance Submodule.addCommGroup {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
        AddCommGroup { x // x p }
        Equations
        theorem Submodule.not_mem_of_ortho {R : Type u} {M : Type v} [inst : Ring R] [inst : IsDomain R] [inst : AddCommGroup M] [inst : Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0) :
        ¬x N
        theorem Submodule.ne_zero_of_ortho {R : Type u} {M : Type v} [inst : Ring R] [inst : IsDomain R] [inst : AddCommGroup M] [inst : Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0) :
        x 0
        instance Submodule.toOrderedAddCommMonoid {R : Type u} [inst : Semiring R] {M : Type u_1} [inst : OrderedAddCommMonoid M] [inst : Module R M] (S : Submodule R M) :

        A submodule of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

        Equations
        • One or more equations did not get rendered due to their size.
        instance Submodule.toLinearOrderedAddCommMonoid {R : Type u} [inst : Semiring R] {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] [inst : Module R M] (S : Submodule R M) :

        A submodule of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

        Equations
        • One or more equations did not get rendered due to their size.
        instance Submodule.toOrderedCancelAddCommMonoid {R : Type u} [inst : Semiring R] {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] [inst : Module R M] (S : Submodule R M) :

        A submodule of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

        Equations
        • One or more equations did not get rendered due to their size.

        A submodule of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

        Equations
        • One or more equations did not get rendered due to their size.
        instance Submodule.toOrderedAddCommGroup {R : Type u} [inst : Ring R] {M : Type u_1} [inst : OrderedAddCommGroup M] [inst : Module R M] (S : Submodule R M) :

        A submodule of an OrderedAddCommGroup is an OrderedAddCommGroup.

        Equations
        • One or more equations did not get rendered due to their size.
        instance Submodule.toLinearOrderedAddCommGroup {R : Type u} [inst : Ring R] {M : Type u_1} [inst : LinearOrderedAddCommGroup M] [inst : Module R M] (S : Submodule R M) :

        A submodule of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

        Equations
        • One or more equations did not get rendered due to their size.
        theorem Submodule.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [inst : DivisionRing S] [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : SMul S R] [inst : Module S M] [inst : IsScalarTower S R M] (p : Submodule R M) {s : S} {x : M} (s0 : s 0) :
        s x p x p
        @[inline]
        abbrev Subspace (R : Type u) (M : Type v) [inst : DivisionRing R] [inst : AddCommGroup M] [inst : Module R M] :

        Subspace of a vector space. Defined to equal Submodule.

        Equations