Documentation

Mathlib.Algebra.Module.Submodule.Basic

Submodules of a module #

In this file we define

• Submodule R M : a subset of a Module M that contains zero and is closed with respect to addition and scalar multiplication.

• Subspace k M : an abbreviation for Submodule assuming that k is a Field.

Tags #

submodule, subspace, linear map

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

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 : ] [inst : ] [inst : Module R M] extends :
• 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
abbrev Submodule.toSubMulAction {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (self : ) :

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 : ] [inst : ] [inst : Module R M] :
SetLike () M
Equations
• One or more equations did not get rendered due to their size.
instance Submodule.addSubmonoidClass {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
Equations
instance Submodule.submoduleClass {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
Equations
• Submodule.submoduleClass = SubmoduleClass.mk
@[simp]
theorem Submodule.mem_toAddSubmonoid {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (p : ) (x : M) :
@[simp]
theorem Submodule.mem_mk {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] {S : } {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 : ] [inst : ] [inst : Module R M] (S : ) (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 : ] [inst : ] [inst : Module R M] {S : } {S' : } (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 : ] [inst : ] [inst : Module R M] {p : } {q : } (h : ∀ (x : M), x p x q) :
p = q
@[simp]
theorem Submodule.carrier_inj {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] {p : } {q : } :
def Submodule.copy {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (p : ) (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 : ] [inst : ] [inst : Module R M] (S : ) (s : Set M) (hs : s = S) :
↑(Submodule.copy S s hs) = s
theorem Submodule.copy_eq {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (S : ) (s : Set M) (hs : s = S) :
Submodule.copy S s hs = S
theorem Submodule.toAddSubmonoid_injective {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
@[simp]
theorem Submodule.toAddSubmonoid_eq {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] {p : } {q : } :
theorem Submodule.toAddSubmonoid_strictMono {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
theorem Submodule.toAddSubmonoid_le {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] {p : } {q : } :
theorem Submodule.toAddSubmonoid_mono {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
@[simp]
theorem Submodule.coe_toAddSubmonoid {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (p : ) :
theorem Submodule.toSubMulAction_injective {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
Function.Injective Submodule.toSubMulAction
theorem Submodule.toSubMulAction_eq {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] {p : } {q : } :
theorem Submodule.toSubMulAction_strictMono {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
StrictMono Submodule.toSubMulAction
theorem Submodule.toSubMulAction_mono {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
Monotone Submodule.toSubMulAction
@[simp]
theorem Submodule.coe_toSubMulAction {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (p : ) :
= p
instance SubmoduleClass.toModule {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] {A : Type u_1} [inst : SetLike A M] [inst : ] [inst : ] (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 : ] [inst : ] [inst : Module R M] {A : Type u_1} [inst : SetLike A M] [inst : ] [inst : ] (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 : ] [inst : ] [inst : Module R M] {A : Type u_1} [inst : SetLike A M] [inst : ] [inst : ] (S' : A) :
↑() = Subtype.val
theorem Submodule.mem_carrier {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) {x : M} :
@[simp]
theorem Submodule.zero_mem {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
0 p
theorem Submodule.add_mem {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) {x : M} {y : M} (h₁ : x p) (h₂ : y p) :
x + y p
theorem Submodule.smul_mem {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) {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 : ] [inst : ] {module_M : Module R M} (p : ) {x : M} [inst : SMul S R] [inst : SMul S M] [inst : ] (r : S) (h : x p) :
r x p
theorem Submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [inst : ] [inst : ] {module_M : Module R M} (p : ) {t : } {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 : ] [inst : ] {module_M : Module R M} (p : ) {t : } {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 : ] [inst : ] {module_M : Module R M} (p : ) {x : M} [inst : ] [inst : ] [inst : SMul G R] [inst : ] (g : G) :
g x p x p
instance Submodule.add {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
Add { x // x p }
Equations
• = { add := fun x y => { val := x + y, property := (_ : x + y p) } }
instance Submodule.zero {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
Zero { x // x p }
Equations
• = { zero := { val := 0, property := (_ : 0 p) } }
instance Submodule.inhabited {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
Inhabited { x // x p }
Equations
• = { default := 0 }
instance Submodule.smul {S : Type u'} {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) [inst : SMul S R] [inst : SMul S M] [inst : ] :
SMul S { x // x p }
Equations
• = { smul := fun c x => { val := c x, property := (_ : c x p) } }
instance Submodule.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) [inst : SMul S R] [inst : SMul S M] [inst : ] :
IsScalarTower S R { x // x p }
Equations
instance Submodule.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) {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 S' { x // x p }
Equations
instance Submodule.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) [inst : SMul S R] [inst : SMul S M] [inst : ] [inst : SMul Sᵐᵒᵖ R] [inst : SMul Sᵐᵒᵖ M] [inst : ] [inst : ] :
IsCentralScalar S { x // x p }
Equations
theorem Submodule.nonempty {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
@[simp]
theorem Submodule.mk_eq_zero {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) {x : M} (h : x p) :
{ val := x, property := h } = 0 x = 0
theorem Submodule.coe_eq_zero {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} {p : } {x : { x // x p }} :
x = 0 x = 0
@[simp]
theorem Submodule.coe_add {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} {p : } (x : { x // x p }) (y : { x // x p }) :
↑(x + y) = x + y
@[simp]
theorem Submodule.coe_zero {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} {p : } :
0 = 0
theorem Submodule.coe_smul {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} {p : } (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 : ] [inst : ] {module_M : Module R M} {p : } [inst : SMul S R] [inst : SMul S M] [inst : ] (r : S) (x : { x // x p }) :
↑(r x) = r x
theorem Submodule.coe_mk {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} {p : } (x : M) (hx : x p) :
{ val := x, property := hx } = x
theorem Submodule.coe_mem {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} {p : } (x : { x // x p }) :
x p
instance Submodule.addCommMonoid {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
AddCommMonoid { x // x p }
Equations
instance Submodule.module' {S : Type u'} {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) [inst : ] [inst : SMul S R] [inst : Module S M] [inst : ] :
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 : ] [inst : ] {module_M : Module R M} (p : ) :
Module R { x // x p }
Equations
instance Submodule.noZeroSMulDivisors {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) [inst : ] :
NoZeroSMulDivisors R { x // x p }
Equations
def Submodule.subtype {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
{ 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 : ] [inst : ] {module_M : Module R M} (p : ) (x : { x // x p }) :
↑() x = x
@[simp]
theorem Submodule.coeSubtype {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
↑() = Subtype.val
theorem Submodule.injective_subtype {R : Type u} {M : Type v} [inst : ] [inst : ] {module_M : Module R M} (p : ) :
theorem Submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [inst : ] [inst : ] {module_M : Module R M} (p : ) (x : ι{ x // x p }) (s : ) :
↑(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 : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (V : ) :

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 : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (V : ) :
↑() = V
@[simp]
theorem Submodule.restrictScalars_mem (S : Type u') {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (V : ) (m : M) :
m V
@[simp]
theorem Submodule.restrictScalars_self {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (V : ) :
theorem Submodule.restrictScalars_injective (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] :
@[simp]
theorem Submodule.restrictScalars_inj (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] {V₁ : } {V₂ : } :
V₁ = V₂
instance Submodule.restrictScalars.origModule (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (p : ) :
Module R { x // }

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

Equations
• = inferInstance
instance Submodule.restrictScalars.isScalarTower (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (p : ) :
IsScalarTower S R { x // }
Equations
@[simp]
theorem Submodule.restrictScalarsEmbedding_apply (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (V : ) :
().toEmbedding V =
def Submodule.restrictScalarsEmbedding (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] :

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 : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (p : ) (a : { x // }) :
↑() a = a
@[simp]
theorem Submodule.restrictScalarsEquiv_symm_apply (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (p : ) (a : { x // x p }) :
↑() a = a
def Submodule.restrictScalarsEquiv (S : Type u') (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : ] [inst : Module S M] [inst : Module R M] [inst : SMul S R] [inst : ] (p : ) :
{ x // } ≃ₗ[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.
instance Submodule.addSubgroupClass {R : Type u} {M : Type v} [inst : Ring R] [inst : ] [inst : Module R M] :
Equations
theorem Submodule.neg_mem {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) {x : M} (hx : x p) :
-x p
def Submodule.toAddSubgroup {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) :

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 : ] {module_M : Module R M} (p : ) :
= p
@[simp]
theorem Submodule.mem_toAddSubgroup {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) {x : M} :
x p
theorem Submodule.toAddSubgroup_injective {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} :
@[simp]
theorem Submodule.toAddSubgroup_eq {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) (p' : ) :
theorem Submodule.toAddSubgroup_strictMono {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} :
theorem Submodule.toAddSubgroup_le {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) (p' : ) :
theorem Submodule.toAddSubgroup_mono {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} :
theorem Submodule.sub_mem {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) {x : M} {y : M} :
x py px - y p
theorem Submodule.neg_mem_iff {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) {x : M} :
-x p x p
theorem Submodule.add_mem_iff_left {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) {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 : ] {module_M : Module R M} (p : ) {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 : ] {module_M : Module R M} (p : ) (x : { x // x p }) :
↑(-x) = -x
theorem Submodule.coe_sub {R : Type u} {M : Type v} [inst : Ring R] [inst : ] {module_M : Module R M} (p : ) (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 : ] {module_M : Module R M} (p : ) {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 : ] {module_M : Module R M} (p : ) {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 : ] {module_M : Module R M} (p : ) :
AddCommGroup { x // x p }
Equations
theorem Submodule.not_mem_of_ortho {R : Type u} {M : Type v} [inst : Ring R] [inst : ] [inst : ] [inst : Module R M] {x : M} {N : } (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 : ] [inst : ] [inst : Module R M] {x : M} {N : } (ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0) :
x 0
instance Submodule.toOrderedAddCommMonoid {R : Type u} [inst : ] {M : Type u_1} [inst : ] [inst : Module R M] (S : ) :

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 : ] {M : Type u_1} [inst : ] [inst : Module R M] (S : ) :

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 : ] {M : Type u_1} [inst : ] [inst : Module R M] (S : ) :

A submodule of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

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

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 : ] [inst : Module R M] (S : ) :

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 : ] [inst : Module R M] (S : ) :

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 : ] [inst : ] [inst : ] [inst : Module R M] [inst : SMul S R] [inst : Module S M] [inst : ] (p : ) {s : S} {x : M} (s0 : s 0) :
s x p x p
@[inline]
abbrev Subspace (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : Module R M] :

Subspace of a vector space. Defined to equal Submodule.

Equations