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.

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}

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}

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}

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}

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

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)

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

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

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

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

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

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

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.

@[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

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)

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

@[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

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.

@[deprecated Submodule.span_induction (since := "2024-10-10")]

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.

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.

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)

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.

@[deprecated Submodule.closure_induction (since := "2024-10-10")]

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.

@[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) = ⊤

@[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} = ⊤

theorem Submodule.span_nat_eq_addSubmonoid_closure {M : Type u_4} [AddCommMonoid M] (s : Set M) : (Submodule.span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

@[simp]

theorem Submodule.span_nat_eq {M : Type u_4} [AddCommMonoid M] (s : AddSubmonoid M) : (Submodule.span ℕ ↑s).toAddSubmonoid = s

theorem Submodule.span_int_eq_addSubgroup_closure {M : Type u_9} [AddCommGroup M] (s : Set M) : (Submodule.span ℤ s).toAddSubgroup = AddSubgroup.closure s

@[simp]

theorem Submodule.span_int_eq {M : Type u_9} [AddCommGroup M] (s : AddSubgroup M) : (Submodule.span ℤ ↑s).toAddSubgroup = s

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 := ⋯ }

@[simp]

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

@[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 = ⊤

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

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)

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)

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)

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)

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)

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))

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}

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}

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

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)

@[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)

@[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

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

@[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)

@[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

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

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

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

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'

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

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}

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})

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

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

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

@[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} = ⊥

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

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}

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}

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}

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}

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

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

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

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

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

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

@[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

@[simp]

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

@[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

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)

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))

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.

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

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

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

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.

theorem Submodule.sup_toAddSubgroup {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

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

theorem Submodule.span_range_update_add_smul {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_8} [DecidableEq ι] {i j : ι} (hij : i ≠ j) (v : ι → M) (r : R) : Submodule.span R (Set.range (Function.update v j (v j + r • v i))) = Submodule.span R (Set.range v)

theorem Submodule.span_range_update_sub_smul {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_8} [DecidableEq ι] {i j : ι} (hij : i ≠ j) (v : ι → M) (r : R) : Submodule.span R (Set.range (Function.update v j (v j - r • v i))) = Submodule.span R (Set.range v)