Documentation

Mathlib.Algebra.Module.Submodule.Basic

Submodules of a module #

In this file we define

Tags #

submodule, subspace, linear map

structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] extends AddSubmonoid :
  • carrier : Set M
  • add_mem' : ∀ {a b : M}, a s.carrierb s.carriera + b s.carrier
  • zero_mem' : 0 s.carrier
  • smul_mem' : ∀ (c : R) {x : M}, x s.carrierc x s.carrier

    The carrier set is closed under scalar multiplication.

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
    @[reducible]
    abbrev Submodule.toSubMulAction {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (self : Submodule R M) :

    Reinterpret a Submodule as a SubMulAction.

    Instances For
      instance Submodule.setLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
      instance Submodule.smulMemClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
      @[simp]
      theorem Submodule.mem_toAddSubmonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] {S : AddSubmonoid M} {x : M} (h : ∀ (c : R) {x : M}, x S.carrierc x S.carrier) :
      x { toAddSubmonoid := S, smul_mem' := h } x S
      @[simp]
      theorem Submodule.coe_set_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : AddSubmonoid M) (h : ∀ (c : R) {x : M}, x S.carrierc x S.carrier) :
      { toAddSubmonoid := S, smul_mem' := h } = S
      @[simp]
      theorem Submodule.eta {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : ∀ (c : R) {x : M}, x p.carrierc x p.carrier) :
      { toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h } = p
      @[simp]
      theorem Submodule.mk_le_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S : AddSubmonoid M} {S' : AddSubmonoid M} (h : ∀ (c : R) {x : M}, x S.carrierc x S.carrier) (h' : ∀ (c : R) {x : M}, x S'.carrierc x S'.carrier) :
      { toAddSubmonoid := S, smul_mem' := h } { toAddSubmonoid := S', smul_mem' := h' } S S'
      theorem Submodule.ext {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :
      p.carrier = q.carrier p = q
      def Submodule.copy {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [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.

      Instances For
        @[simp]
        theorem Submodule.coe_copy {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] :
        Function.Injective Submodule.toAddSubmonoid
        @[simp]
        theorem Submodule.toAddSubmonoid_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] :
        StrictMono Submodule.toAddSubmonoid
        theorem Submodule.toAddSubmonoid_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] :
        Monotone Submodule.toAddSubmonoid
        @[simp]
        theorem Submodule.coe_toAddSubmonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        p.toAddSubmonoid = p
        theorem Submodule.toSubMulAction_injective {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        Function.Injective Submodule.toSubMulAction
        theorem Submodule.toSubMulAction_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        StrictMono Submodule.toSubMulAction
        theorem Submodule.toSubMulAction_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        Monotone Submodule.toSubMulAction
        @[simp]
        theorem Submodule.coe_toSubMulAction {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        instance SMulMemClass.toModule {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] [SMulMemClass A R M] (S' : A) :
        Module R { x // x S' }

        A submodule of a Module is a Module.

        def SMulMemClass.toModule' (S : Type u_2) (R' : Type u_3) (R : Type u_4) (A : Type u_5) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SetLike S A] [AddSubmonoidClass S A] [SMulMemClass S R A] (s : S) :
        Module R' { x // x s }

        This can't be an instance because Lean wouldn't know how to find R, but we can still use this to manually derive Module on specific types.

        Instances For
          def SMulMemClass.subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] [SMulMemClass 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.

          Instances For
            @[simp]
            theorem SMulMemClass.coeSubtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] [SMulMemClass A R M] (S' : A) :
            ↑(SMulMemClass.subtype S') = Subtype.val
            theorem Submodule.mem_carrier {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} :
            x p.carrier x p
            @[simp]
            theorem Submodule.zero_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
            0 p
            theorem Submodule.add_mem {R : Type u} {M : Type v} [Semiring R] [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} [Semiring R] [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} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x p) :
            r x p
            theorem Submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [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} [Semiring R] [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} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) :
            g x p x p
            instance Submodule.add {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
            Add { x // x p }
            instance Submodule.zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
            Zero { x // x p }
            instance Submodule.inhabited {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
            Inhabited { x // x p }
            instance Submodule.smul {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] :
            SMul S { x // x p }
            instance Submodule.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] :
            IsScalarTower S R { x // x p }
            instance Submodule.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {S' : Type u_1} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S'] [IsScalarTower S' R M] [IsScalarTower S S' M] [IsScalarTower S R M] :
            IsScalarTower S S' { x // x p }
            instance Submodule.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :
            IsCentralScalar S { x // x p }
            theorem Submodule.nonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
            @[simp]
            theorem Submodule.mk_eq_zero {R : Type u} {M : Type v} [Semiring R] [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} [Semiring R] [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} [Semiring R] [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} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} :
            0 = 0
            theorem Submodule.coe_smul {R : Type u} {M : Type v} [Semiring R] [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} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : { x // x p }) :
            ↑(r x) = r x
            theorem Submodule.coe_mk {R : Type u} {M : Type v} [Semiring R] [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} [Semiring R] [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} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
            AddCommMonoid { x // x p }
            instance Submodule.module' {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
            Module S { x // x p }
            instance Submodule.module {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
            Module R { x // x p }
            instance Submodule.noZeroSMulDivisors {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [NoZeroSMulDivisors R M] :
            NoZeroSMulDivisors R { x // x p }
            def Submodule.subtype {R : Type u} {M : Type v} [Semiring R] [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.

            Instances For
              theorem Submodule.subtype_apply {R : Type u} {M : Type v} [Semiring R] [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} [Semiring R] [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} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
              theorem Submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [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.

              Additive actions by Submodules #

              These instances transfer the action by an element m : M of an R-module M written as m +ᵥ a onto the action by an element s : S of a submodule S : Submodule R M such that s +ᵥ a = (s : M) +ᵥ a. These instances work particularly well in conjunction with AddGroup.toAddAction, enabling s +ᵥ m as an alias for ↑s + m.

              instance Submodule.instVAddSubtypeMemSubmoduleInstMembershipSetLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [VAdd M α] :
              VAdd { x // x p } α
              instance Submodule.vaddCommClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} {β : Type u_2} [VAdd M β] [VAdd α β] [VAddCommClass M α β] :
              VAddCommClass { x // x p } α β

              The action by a submodule is the action by the underlying module.

              theorem Submodule.vadd_def {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {α : Type u_1} [VAdd M α] (g : { x // x p }) (m : α) :
              g +ᵥ m = g +ᵥ m
              def Submodule.restrictScalars (S : Type u') {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [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.

              Instances For
                @[simp]
                theorem Submodule.coe_restrictScalars (S : Type u') {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :
                @[simp]
                theorem Submodule.restrictScalars_mem (S : Type u') {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) (m : M) :
                @[simp]
                @[simp]
                theorem Submodule.restrictScalars_inj (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [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) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :

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

                instance Submodule.restrictScalars.isScalarTower (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :
                def Submodule.restrictScalarsEmbedding (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] :

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

                Instances For
                  @[simp]
                  theorem Submodule.restrictScalarsEquiv_symm_apply (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :
                  ∀ (a : { x // x p }), ↑(LinearEquiv.symm (Submodule.restrictScalarsEquiv S R M p)) a = a
                  @[simp]
                  theorem Submodule.restrictScalarsEquiv_apply (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :
                  ∀ (a : { x // x p }), ↑(Submodule.restrictScalarsEquiv S R M p) a = a
                  def Submodule.restrictScalarsEquiv (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [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.

                  Instances For
                    theorem Submodule.neg_mem {R : Type u} {M : Type v} [Ring R] [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} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

                    Reinterpret a submodule as an additive subgroup.

                    Instances For
                      @[simp]
                      theorem Submodule.coe_toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
                      @[simp]
                      theorem Submodule.mem_toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} :
                      theorem Submodule.toAddSubgroup_injective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :
                      Function.Injective Submodule.toAddSubgroup
                      @[simp]
                      theorem Submodule.toAddSubgroup_eq {R : Type u} {M : Type v} [Ring R] [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} [Ring R] [AddCommGroup M] {module_M : Module R M} :
                      StrictMono Submodule.toAddSubgroup
                      theorem Submodule.toAddSubgroup_le {R : Type u} {M : Type v} [Ring R] [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} [Ring R] [AddCommGroup M] {module_M : Module R M} :
                      Monotone Submodule.toAddSubgroup
                      theorem Submodule.sub_mem {R : Type u} {M : Type v} [Ring R] [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} [Ring R] [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} [Ring R] [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} [Ring R] [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} [Ring R] [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} [Ring R] [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} [Ring R] [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} [Ring R] [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} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
                      AddCommGroup { x // x p }
                      theorem Submodule.not_mem_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [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} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0) :
                      x 0
                      instance Submodule.toOrderedAddCommGroup {R : Type u} [Ring R] {M : Type u_1} [OrderedAddCommGroup M] [Module R M] (S : Submodule R M) :

                      A submodule of an OrderedAddCommGroup is an OrderedAddCommGroup.

                      theorem Submodule.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [DivisionSemiring S] [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M] (p : Submodule R M) {s : S} {x : M} (s0 : s 0) :
                      s x p x p
                      @[inline, reducible]
                      abbrev Subspace (R : Type u) (M : Type v) [DivisionRing R] [AddCommGroup M] [Module R M] :

                      Subspace of a vector space. Defined to equal Submodule.

                      Instances For