The span of a set of vectors, as a submodule #

Submodule.span s is defined to be the smallest submodule containing the set s.

Notations #

We introduce the notation R ∙ v for the span of a singleton, Submodule.span R {v}. This is \span, not the same as the scalar multiplication •/\bub.

source

def Submodule.span (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :

Submodule R M

The span of a set s ⊆ M is the smallest submodule of M that contains s.

Equations

Submodule.span R s = sInf {p : Submodule R M | s ⊆ ↑p}

Instances For

source

class Submodule.IsPrincipal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) :

Prop

An R-submodule of M is principal if it is generated by one element.

principal' : ∃ (a : M), S = Submodule.span R {a}

Instances

source

theorem Submodule.isPrincipal_iff {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) :

S.IsPrincipal ↔ ∃ (a : M), S = Submodule.span R {a}

source

theorem Submodule.IsPrincipal.principal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) [S.IsPrincipal] :

∃ (a : M), S = Submodule.span R {a}

source

theorem Submodule.mem_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} :

x ∈ Submodule.span R s ↔ ∀ (p : Submodule R M), s ⊆ ↑p → x ∈ p

source

theorem Submodule.subset_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

s ⊆ ↑(Submodule.span R s)

source

theorem Submodule.span_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : Submodule R M} :

Submodule.span R s ≤ p ↔ s ⊆ ↑p

source

theorem Submodule.span_mono {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set M} (h : s ⊆ t) :

Submodule.span R s ≤ Submodule.span R t

source

theorem Submodule.span_monotone {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :

Monotone (Submodule.span R)

source

theorem Submodule.span_eq_of_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {s : Set M} (h₁ : s ⊆ ↑p) (h₂ : p ≤ Submodule.span R s) :

Submodule.span R s = p

source

theorem Submodule.span_eq {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

Submodule.span R ↑p = p

source

theorem Submodule.span_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set M} (hs : s ⊆ ↑(Submodule.span R t)) (ht : t ⊆ ↑(Submodule.span R s)) :

Submodule.span R s = Submodule.span R t

source

theorem Submodule.coe_span_eq_self {R : Type u_1} {M : Type u_4} {S : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :

↑(Submodule.span R ↑s) = ↑s

A version of Submodule.span_eq for subobjects closed under addition and scalar multiplication and containing zero. In general, this should not be used directly, but can be used to quickly generate proofs for specific types of subobjects.

source

@[simp]

theorem Submodule.span_insert_zero {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

Submodule.span R (insert 0 s) = Submodule.span R s

source

theorem Submodule.closure_subset_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

↑(AddSubmonoid.closure s) ⊆ ↑(Submodule.span R s)

source

theorem Submodule.closure_le_toAddSubmonoid_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

AddSubmonoid.closure s ≤ (Submodule.span R s).toAddSubmonoid

source

@[simp]

theorem Submodule.span_closure {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

Submodule.span R ↑(AddSubmonoid.closure s) = Submodule.span R s

source

theorem Submodule.span_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x ∈ Submodule.span R s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) (smul : ∀ (a : R) (x : M) (hx : x ∈ Submodule.span R s), p x hx → p (a • x) ⋯) {x : M} (hx : x ∈ Submodule.span R s) :

p x hx

An induction principle for span membership. If p holds for 0 and all elements of s, and is preserved under addition and scalar multiplication, then p holds for all elements of the span of s.

source

@[deprecated Submodule.span_induction]

theorem Submodule.span_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x ∈ Submodule.span R s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) (smul : ∀ (a : R) (x : M) (hx : x ∈ Submodule.span R s), p x hx → p (a • x) ⋯) {x : M} (hx : x ∈ Submodule.span R s) :

p x hx

Alias of Submodule.span_induction.

An induction principle for span membership. If p holds for 0 and all elements of s, and is preserved under addition and scalar multiplication, then p holds for all elements of the span of s.

source

theorem Submodule.span_induction₂ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x y : M) → x ∈ Submodule.span R s → y ∈ Submodule.span R s → Prop} (mem_mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (y : M) (hy : y ∈ Submodule.span R s), p 0 y ⋯ hy) (zero_right : ∀ (x : M) (hx : x ∈ Submodule.span R s), p x 0 hx ⋯) (add_left : ∀ (x y z : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s) (hz : z ∈ Submodule.span R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s) (hz : z ∈ Submodule.span R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (smul_left : ∀ (r : R) (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x y hx hy → p (r • x) y ⋯ hy) (smul_right : ∀ (r : R) (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x y hx hy → p x (r • y) hx ⋯) {a b : M} (ha : a ∈ Submodule.span R s) (hb : b ∈ Submodule.span R s) :

p a b ha hb

An induction principle for span membership. This is a version of Submodule.span_induction for binary predicates.

source

theorem Submodule.span_eq_closure {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

(Submodule.span R s).toAddSubmonoid = AddSubmonoid.closure (Set.univ • s)

source

theorem Submodule.closure_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x ∈ Submodule.span R s → Prop} (zero : p 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) (smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯) {x : M} (hx : x ∈ Submodule.span R s) :

p x hx

A variant of span_induction that combines ∀ x ∈ s, p x and ∀ r x, p x → p (r • x) into a single condition ∀ r, ∀ x ∈ s, p (r • x), which can be easier to verify.

source

@[deprecated Submodule.closure_induction]

theorem Submodule.closure_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x ∈ Submodule.span R s → Prop} (zero : p 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) (smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯) {x : M} (hx : x ∈ Submodule.span R s) :

p x hx

Alias of Submodule.closure_induction.

A variant of span_induction that combines ∀ x ∈ s, p x and ∀ r x, p x → p (r • x) into a single condition ∀ r, ∀ x ∈ s, p (r • x), which can be easier to verify.

source

@[simp]

theorem Submodule.span_span_coe_preimage {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

Submodule.span R (Subtype.val ⁻¹' s) = ⊤

source

@[simp]

theorem Submodule.span_setOf_mem_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

Submodule.span R {x : ↥(Submodule.span R s) | ↑x ∈ s} = ⊤

source

theorem Submodule.span_nat_eq_addSubmonoid_closure {M : Type u_4} [AddCommMonoid M] (s : Set M) :

(Submodule.span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

source

@[simp]

theorem Submodule.span_nat_eq {M : Type u_4} [AddCommMonoid M] (s : AddSubmonoid M) :

(Submodule.span ℕ ↑s).toAddSubmonoid = s

source

theorem Submodule.span_int_eq_addSubgroup_closure {M : Type u_9} [AddCommGroup M] (s : Set M) :

(Submodule.span ℤ s).toAddSubgroup = AddSubgroup.closure s

source

@[simp]

theorem Submodule.span_int_eq {M : Type u_9} [AddCommGroup M] (s : AddSubgroup M) :

(Submodule.span ℤ ↑s).toAddSubgroup = s

source

def Submodule.gi (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] :

GaloisInsertion (Submodule.span R) SetLike.coe

span forms a Galois insertion with the coercion from submodule to set.

Equations

Submodule.gi R M = { choice := fun (s : Set M) (x : ↑(Submodule.span R s) ≤ s) => Submodule.span R s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

Instances For

source

@[simp]

theorem Submodule.span_empty {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :

Submodule.span R ∅ = ⊥

source

@[simp]

theorem Submodule.span_univ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :

Submodule.span R Set.univ = ⊤

source

theorem Submodule.span_union {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set M) :

Submodule.span R (s ∪ t) = Submodule.span R s ⊔ Submodule.span R t

source

theorem Submodule.span_iUnion {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (s : ι → Set M) :

Submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), Submodule.span R (s i)

source

theorem Submodule.span_iUnion₂ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_10} {κ : ι → Sort u_9} (s : (i : ι) → κ i → Set M) :

Submodule.span R (⋃ (i : ι), ⋃ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), Submodule.span R (s i j)

source

theorem Submodule.span_attach_biUnion {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq M] {α : Type u_9} (s : Finset α) (f : { x : α // x ∈ s } → Finset M) :

Submodule.span R ↑(s.attach.biUnion f) = ⨆ (x : { x : α // x ∈ s }), Submodule.span R ↑(f x)

source

theorem Submodule.sup_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {s : Set M} :

p ⊔ Submodule.span R s = Submodule.span R (↑p ∪ s)

source

theorem Submodule.span_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {s : Set M} :

Submodule.span R s ⊔ p = Submodule.span R (s ∪ ↑p)

source

def Submodule.«term_∙_» :

Lean.TrailingParserDescr

Equations

Submodule.«term_∙_» = Lean.ParserDescr.trailingNode `Submodule.«term_∙_» 1000 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 0))

Instances For

source

theorem Submodule.span_eq_iSup_of_singleton_spans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :

Submodule.span R s = ⨆ x ∈ s, Submodule.span R {x}

source

theorem Submodule.span_range_eq_iSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} {v : ι → M} :

Submodule.span R (Set.range v) = ⨆ (i : ι), Submodule.span R {v i}

source

theorem Submodule.span_smul_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (r : R) :

Submodule.span R (r • s) ≤ Submodule.span R s

source

theorem Submodule.subset_span_trans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {U V W : Set M} (hUV : U ⊆ ↑(Submodule.span R V)) (hVW : V ⊆ ↑(Submodule.span R W)) :

U ⊆ ↑(Submodule.span R W)

source

@[simp]

theorem Submodule.coe_iSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) S) :

↑(iSup S) = ⋃ (i : ι), ↑(S i)

source

@[simp]

theorem Submodule.mem_iSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) S) {x : M} :

x ∈ iSup S ↔ ∃ (i : ι), x ∈ S i

source

theorem Submodule.mem_sSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Submodule R M)} {z : M} (hs : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : Submodule R M) => x1 ≤ x2) s) :

z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

source

@[simp]

theorem Submodule.coe_iSup_of_chain {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (a : ℕ →o Submodule R M) :

↑(⨆ (k : ℕ), a k) = ⋃ (k : ℕ), ↑(a k)

source

@[simp]

theorem Submodule.mem_iSup_of_chain {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (a : ℕ →o Submodule R M) (m : M) :

m ∈ ⨆ (k : ℕ), a k ↔ ∃ (k : ℕ), m ∈ a k

source

theorem Submodule.mem_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {p p' : Submodule R M} :

x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x

source

theorem Submodule.mem_sup' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {p p' : Submodule R M} :

x ∈ p ⊔ p' ↔ ∃ (y : ↥p) (z : ↥p'), ↑y + ↑z = x

source

theorem Submodule.exists_add_eq_of_codisjoint {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} (h : Codisjoint p p') (x : M) :

∃ y ∈ p, ∃ z ∈ p', y + z = x

source

theorem Submodule.coe_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) :

↑(p ⊔ p') = ↑p + ↑p'

source

theorem Submodule.sup_toAddSubmonoid {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) :

(p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid

source

theorem Submodule.sup_toAddSubgroup {R : Type u_9} {M : Type u_10} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) :

(p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

source

theorem Submodule.mem_span_singleton_self {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :

x ∈ Submodule.span R {x}

source

theorem Submodule.nontrivial_span_singleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} (h : x ≠ 0) :

Nontrivial ↥(Submodule.span R {x})

source

theorem Submodule.mem_span_singleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x y : M} :

x ∈ Submodule.span R {y} ↔ ∃ (a : R), a • y = x

source

theorem Submodule.le_span_singleton_iff {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Submodule R M} {v₀ : M} :

s ≤ Submodule.span R {v₀} ↔ ∀ v ∈ s, ∃ (r : R), r • v₀ = v

source

theorem Submodule.span_singleton_eq_top_iff (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :

Submodule.span R {x} = ⊤ ↔ ∀ (v : M), ∃ (r : R), r • x = v

source

@[simp]

theorem Submodule.span_zero_singleton (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :

Submodule.span R {0} = ⊥

source

theorem Submodule.span_singleton_eq_range (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (y : M) :

↑(Submodule.span R {y}) = Set.range fun (x : R) => x • y

source

theorem Submodule.span_singleton_smul_le (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_9} [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (r : S) (x : M) :

Submodule.span R {r • x} ≤ Submodule.span R {x}

source

theorem Submodule.span_singleton_group_smul_eq (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_9} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) (x : M) :

Submodule.span R {g • x} = Submodule.span R {x}

source

theorem Submodule.span_singleton_smul_eq {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} (hr : IsUnit r) (x : M) :

Submodule.span R {r • x} = Submodule.span R {x}

source

theorem Submodule.mem_span_singleton_trans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x y z : M} (hxy : x ∈ Submodule.span R {y}) (hyz : y ∈ Submodule.span R {z}) :

x ∈ Submodule.span R {z}

source

theorem Submodule.span_insert {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (s : Set M) :

Submodule.span R (insert x s) = Submodule.span R {x} ⊔ Submodule.span R s

source

theorem Submodule.span_insert_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} (h : x ∈ Submodule.span R s) :

Submodule.span R (insert x s) = Submodule.span R s

source

theorem Submodule.span_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

Submodule.span R ↑(Submodule.span R s) = Submodule.span R s

source

theorem Submodule.mem_span_insert {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} {y : M} :

x ∈ Submodule.span R (insert y s) ↔ ∃ (a : R), ∃ z ∈ Submodule.span R s, x = a • y + z

source

theorem Submodule.mem_span_pair {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x y z : M} :

z ∈ Submodule.span R {x, y} ↔ ∃ (a : R) (b : R), a • x + b • y = z

source

theorem Submodule.span_eq_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :

Submodule.span R s = ⊥ ↔ ∀ x ∈ s, x = 0

source

@[simp]

theorem Submodule.span_singleton_eq_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :

Submodule.span R {x} = ⊥ ↔ x = 0

source

@[simp]

theorem Submodule.span_zero {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :

Submodule.span R 0 = ⊥

source

@[simp]

theorem Submodule.span_singleton_le_iff_mem {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (m : M) (p : Submodule R M) :

Submodule.span R {m} ≤ p ↔ m ∈ p

source

theorem Submodule.iSup_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Set M) :

⨆ (i : ι), Submodule.span R (p i) = Submodule.span R (⋃ (i : ι), p i)

source

theorem Submodule.iSup_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Submodule R M) :

⨆ (i : ι), p i = Submodule.span R (⋃ (i : ι), ↑(p i))

source

theorem Submodule.submodule_eq_sSup_le_nonzero_spans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

p = sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = Submodule.span R {m}}

A submodule is equal to the supremum of the spans of the submodule's nonzero elements.

source

theorem Submodule.lt_sup_iff_not_mem {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {I : Submodule R M} {a : M} :

I < I ⊔ Submodule.span R {a} ↔ a ∉ I

source

theorem Submodule.mem_iSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Submodule R M) {m : M} :

m ∈ ⨆ (i : ι), p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

source

theorem Submodule.mem_sSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Submodule R M)} {m : M} :

m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N

source

theorem Submodule.mem_span_finite_of_mem_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set M} {x : M} (hx : x ∈ Submodule.span R S) :

∃ (T : Finset M), ↑T ⊆ S ∧ x ∈ Submodule.span R ↑T

For every element in the span of a set, there exists a finite subset of the set such that the element is contained in the span of the subset.

source

theorem Submodule.mem_span_insert' {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {x y : M} {s : Set M} :

x ∈ Submodule.span R (insert y s) ↔ ∃ (a : R), x + a • y ∈ Submodule.span R s

HepLean Documentation

Mathlib.LinearAlgebra.Span.Defs

The span of a set of vectors, as a submodule #

Notations #