Linear independence

This file defines linear independence in a module or vector space.

It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.

We define LinearIndependent R v as Function.Injective (Finsupp.linearCombination R v). Here Finsupp.linearCombination is the linear map sending a function f : ι →₀ R with finite support to the linear combination of vectors from v with these coefficients.

The goal of this file is to define linear independence and to prove that several other statements are equivalent to this one, including ker (Finsupp.linearCombination R v) = ⊥ and some versions with explicitly written linear combinations.

Main definitions

All definitions are given for families of vectors, i.e. v : ι → M where M is the module or vector space and ι : Type* is an arbitrary indexing type.

• LinearIndependent R v states that the elements of the family v are linearly independent.

• LinearIndepOn R v s states that the elements of the family v indexed by the members of the set s : Set ι are linearly independent.

• LinearIndependent.repr hv x returns the linear combination representing x : span R (range v) on the linearly independent vectors v, given hv : LinearIndependent R v (using classical choice). LinearIndependent.repr hv is provided as a linear map.

• LinearIndependent.Maximal states that there exists no linear independent family that strictly includes the given one.

Main results

• Fintype.linearIndependent_iff: if ι is a finite type, then any function f : ι → R has finite support, so we can reformulate the statement using ∑ i : ι, f i • v i instead of a sum over an auxiliary s : Finset ι;

Implementation notes

We use families instead of sets because it allows us to say that two identical vectors are linearly dependent.

If you want to use sets, use the family (fun x ↦ x : s → M) given a set s : Set M. The lemmas LinearIndependent.to_subtype_range and LinearIndependent.of_subtype_range connect those two worlds.

TODO

Rework proofs to hold in semirings, by avoiding the path through ker (Finsupp.linearCombination R v) = ⊥.

Tags

linearly dependent, linear dependence, linearly independent, linear independence

def LinearIndependent {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop

LinearIndependent R v states the family of vectors v is linearly independent over R.

Equations

• LinearIndependent R v = Function.Injective ⇑(Finsupp.linearCombination R v)

def delabLinearIndependent : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for LinearIndependent that suggests pretty printing with type hints in case the family of vectors is over a Set.

Type hints look like LinearIndependent fun (v : ↑s) => ↑v or LinearIndependent (ι := ↑s) f, depending on whether the family is a lambda expression or not.

Equations

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

def LinearIndepOn {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set ι) : Prop

LinearIndepOn R v s states that the vectors in the family v that are indexed by the elements of s are linearly independent over R.

Equations

• LinearIndepOn R v s = LinearIndependent R fun (x : ↑s) => v ↑x

theorem LinearIndepOn.linearIndependent {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set ι} (h : LinearIndepOn R v s) : LinearIndependent R fun (x : ↑s) => v ↑x

theorem linearIndependent_iff_injective_linearCombination {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ Function.Injective ⇑(Finsupp.linearCombination R v)

theorem LinearIndependent.injective_linearCombination {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v → Function.Injective ⇑(Finsupp.linearCombination R v)

Alias of the forward direction of linearIndependent_iff_injective_linearCombination.

theorem Fintype.linearIndependent_iff_injective {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] : LinearIndependent R v ↔ Function.Injective ⇑((Fintype.linearCombination R ℕ) v)

theorem LinearIndependent.injective {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (hv : LinearIndependent R v) : Function.Injective v

theorem LinearIndepOn.injOn {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (hv : LinearIndepOn R v s) : Set.InjOn v s

theorem LinearIndependent.ne_zero {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (i : ι) (hv : LinearIndependent R v) : v i ≠ 0

theorem LinearIndepOn.ne_zero {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {i : ι} (hv : LinearIndepOn R v s) (hi : i ∈ s) : v i ≠ 0

theorem linearIndependent_empty_type {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [IsEmpty ι] : LinearIndependent R v

@[simp]

theorem linearIndependent_zero_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] : LinearIndependent R 0 ↔ IsEmpty ι

theorem linearIndependent_empty (R : Type u_2) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R fun (x : ↑∅) => ↑x

@[simp]

theorem linearIndepOn_empty {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v ∅

theorem linearIndependent_set_coe_iff {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : (LinearIndependent R fun (x : ↑s) => v ↑x) ↔ LinearIndepOn R v s

@[deprecated linearIndependent_set_coe_iff (since := "2025-02-20")]

theorem linearIndependent_set_subtype {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : (LinearIndependent R fun (x : ↑s) => v ↑x) ↔ LinearIndepOn R v s

Alias of linearIndependent_set_coe_iff.

theorem linearIndependent_subtype_iff {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : LinearIndependent R Subtype.val ↔ LinearIndepOn R id s

theorem linearIndependent_comp_subtype_iff {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ LinearIndepOn R v s

theorem LinearIndependent.comp {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (h : LinearIndependent R v) (f : ι' → ι) (hf : Function.Injective f) : LinearIndependent R (v ∘ f)

A subfamily of a linearly independent family (i.e., a composition with an injective map) is a linearly independent family.

theorem linearIndependent_iffₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂

theorem linearIndependent_iff'ₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

theorem linearIndependent_iff''ₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i

theorem not_linearIndependent_iffₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : ¬LinearIndependent R v ↔ ∃ (s : Finset ι) (f : ι → R) (g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

theorem Fintype.linearIndependent_iffₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] : LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i : ι, f i • v i = ∑ i : ι, g i • v i → ∀ (i : ι), f i = g i

theorem Fintype.not_linearIndependent_iffₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] : ¬LinearIndependent R v ↔ ∃ (f : ι → R) (g : ι → R), ∑ i : ι, f i • v i = ∑ i : ι, g i • v i ∧ ∃ (i : ι), f i ≠ g i

theorem linearIndependent_iff_finset_linearIndependent {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)

A family is linearly independent if and only if all of its finite subfamily is linearly independent.

theorem LinearIndependent.of_comp {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (hfv : LinearIndependent R (⇑f ∘ v)) : LinearIndependent R v

If the image of a family of vectors under a linear map is linearly independent, then so is the original family.

theorem LinearIndepOn.of_comp {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {M' : Type u_5} {v : ι → M} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (hfv : LinearIndepOn R (⇑f ∘ v) s) : LinearIndepOn R v s

theorem LinearMap.linearIndependent_iff_of_injOn {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (hf_inj : Set.InjOn ⇑f ↑(Submodule.span R (Set.range v))) : LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v

If f is a linear map injective on the span of the range of v, then the family f ∘ v is linearly independent if and only if the family v is linearly independent. See LinearMap.linearIndependent_iff_of_disjoint for the version with Set.InjOn replaced by Disjoint when working over a ring.

theorem LinearMap.linearIndepOn_iff_of_injOn {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {M' : Type u_5} {v : ι → M} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (hf_inj : Set.InjOn ⇑f ↑(Submodule.span R (v '' s))) : LinearIndepOn R (⇑f ∘ v) s ↔ LinearIndepOn R v s

theorem linearIndependent_of_subsingleton {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] : LinearIndependent R v

theorem LinearIndepOn.of_subsingleton {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] : LinearIndepOn R v s

theorem linearIndependent_equiv {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (e : ι ≃ ι') {f : ι' → M} : LinearIndependent R (f ∘ ⇑e) ↔ LinearIndependent R f

theorem linearIndependent_equiv' {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (e : ι ≃ ι') {f : ι' → M} {g : ι → M} (h : f ∘ ⇑e = g) : LinearIndependent R g ↔ LinearIndependent R f

theorem linearIndepOn_equiv {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (e : ι ≃ ι') {f : ι' → M} {s : Set ι} : LinearIndepOn R (f ∘ ⇑e) s ↔ LinearIndepOn R f (⇑e '' s)

@[simp]

theorem linearIndepOn_univ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v Set.univ ↔ LinearIndependent R v

theorem LinearIndependent.linearIndepOn {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v → LinearIndepOn R v Set.univ

Alias of the reverse direction of linearIndepOn_univ.

theorem linearIndepOn_iff_image {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {s : Set ι} {f : ι → M} (hf : Set.InjOn f s) : LinearIndepOn R f s ↔ LinearIndepOn R id (f '' s)

@[deprecated linearIndepOn_iff_image (since := "2025-02-14")]

theorem linearIndependent_image {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {s : Set ι} {f : ι → M} (hf : Set.InjOn f s) : LinearIndepOn R f s ↔ LinearIndepOn R id (f '' s)

Alias of linearIndepOn_iff_image.

theorem linearIndepOn_range_iff {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {f : ι → ι'} (hf : Function.Injective f) (g : ι' → M) : LinearIndepOn R g (Set.range f) ↔ LinearIndependent R (g ∘ f)

theorem LinearIndependent.of_linearIndepOn_range {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {f : ι → ι'} (hf : Function.Injective f) (g : ι' → M) : LinearIndepOn R g (Set.range f) → LinearIndependent R (g ∘ f)

Alias of the forward direction of linearIndepOn_range_iff.

theorem linearIndepOn_id_range_iff {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {f : ι → M} (hf : Function.Injective f) : LinearIndepOn R id (Set.range f) ↔ LinearIndependent R f

theorem LinearIndependent.of_linearIndepOn_id_range {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {f : ι → M} (hf : Function.Injective f) : LinearIndepOn R id (Set.range f) → LinearIndependent R f

Alias of the forward direction of linearIndepOn_id_range_iff.

@[deprecated linearIndepOn_id_range_iff (since := "2025-02-15")]

theorem linearIndependent_subtype_range {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {f : ι → M} (hf : Function.Injective f) : LinearIndepOn R id (Set.range f) ↔ LinearIndependent R f

Alias of linearIndepOn_id_range_iff.

@[deprecated LinearIndependent.of_linearIndepOn_id_range (since := "2025-02-15")]

theorem LinearIndependent.of_subtype_range {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} {f : ι → M} (hf : Function.Injective f) : LinearIndepOn R id (Set.range f) → LinearIndependent R f

Alias of the forward direction of linearIndepOn_id_range_iff.

---

Alias of the forward direction of linearIndepOn_id_range_iff.

theorem LinearIndependent.linearIndepOn_id {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (i : LinearIndependent R v) : LinearIndepOn R id (Set.range v)

@[deprecated LinearIndependent.linearIndepOn_id (since := "2025-02-15")]

theorem LinearIndependent.to_subtype_range {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (i : LinearIndependent R v) : LinearIndepOn R id (Set.range v)

Alias of LinearIndependent.linearIndepOn_id.

@[deprecated LinearIndependent.linearIndepOn_id (since := "2025-02-14")]

theorem LinearIndependent.coe_range {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (i : LinearIndependent R v) : LinearIndepOn R id (Set.range v)

Alias of LinearIndependent.linearIndepOn_id.

theorem LinearIndependent.linearIndepOn_id' {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) {t : Set M} (ht : Set.range v = t) : LinearIndepOn R id t

A version of LinearIndependent.linearIndepOn_id with the set range equality as a hypothesis.

@[deprecated LinearIndependent.linearIndepOn_id' (since := "2025-02-16")]

theorem LinearIndependent.to_subtype_range' {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) {t : Set M} (ht : Set.range v = t) : LinearIndepOn R id t

Alias of LinearIndependent.linearIndepOn_id'.

---

A version of LinearIndependent.linearIndepOn_id with the set range equality as a hypothesis.

theorem linearIndepOn_iffₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g

@[deprecated linearIndepOn_iffₛ (since := "2025-02-15")]

theorem linearIndependent_comp_subtypeₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g

Alias of linearIndepOn_iffₛ.

theorem linearDepOn_iff'ₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ (f : ι →₀ R) (g : ι →₀ R), f ∈ Finsupp.supported R R s ∧ g ∈ Finsupp.supported R R s ∧ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g ∧ f ≠ g

An indexed set of vectors is linearly dependent iff there are two distinct Finsupp.LinearCombinations of the vectors with the same value.

@[deprecated linearDepOn_iff'ₛ (since := "2025-02-15")]

theorem linearDependent_comp_subtype'ₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ (f : ι →₀ R) (g : ι →₀ R), f ∈ Finsupp.supported R R s ∧ g ∈ Finsupp.supported R R s ∧ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g ∧ f ≠ g

Alias of linearDepOn_iff'ₛ.

---

An indexed set of vectors is linearly dependent iff there are two distinct Finsupp.LinearCombinations of the vectors with the same value.

theorem linearDepOn_iffₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ (f : ι →₀ R) (g : ι →₀ R), f ∈ Finsupp.supported R R s ∧ g ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = ∑ i ∈ g.support, g i • v i ∧ f ≠ g

A version of linearDepOn_iff'ₛ with Finsupp.linearCombination unfolded.

@[deprecated linearDepOn_iffₛ (since := "2025-02-15")]

theorem linearDependent_comp_subtypeₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ (f : ι →₀ R) (g : ι →₀ R), f ∈ Finsupp.supported R R s ∧ g ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = ∑ i ∈ g.support, g i • v i ∧ f ≠ g

Alias of linearDepOn_iffₛ.

---

A version of linearDepOn_iff'ₛ with Finsupp.linearCombination unfolded.

@[deprecated linearIndepOn_iffₛ (since := "2025-02-15")]

theorem linearIndependent_subtypeₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g

Alias of linearIndepOn_iffₛ.

theorem linearIndependent_restrict_iff {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent (ι := ↑s) R (s.restrict v) ↔ LinearIndepOn R v s

theorem LinearIndepOn.linearIndependent_restrict {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hs : LinearIndepOn R v s) : LinearIndependent (ι := ↑s) R (s.restrict v)

@[deprecated LinearIndepOn.linearIndependent_restrict (since := "2025-02-15")]

theorem LinearIndependent.restrict_of_comp_subtype {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hs : LinearIndepOn R v s) : LinearIndependent (ι := ↑s) R (s.restrict v)

Alias of LinearIndepOn.linearIndependent_restrict.

theorem linearIndepOn_iff_linearCombinationOnₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ Function.Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

@[deprecated linearIndepOn_iff_linearCombinationOnₛ (since := "2025-02-15")]

theorem linearIndependent_iff_linearCombinationOnₛ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ Function.Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Alias of linearIndepOn_iff_linearCombinationOnₛ.

def LinearIndependent.linearCombinationEquiv {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : (ι →₀ R) ≃ₗ[R] ↥(Submodule.span R (Set.range v))

Canonical isomorphism between linear combinations and the span of linearly independent vectors.

Equations

• hv.linearCombinationEquiv = LinearEquiv.ofBijective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯) ⋯

@[simp]

theorem LinearIndependent.linearCombinationEquiv_symm_apply {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (a✝ : ↥(Submodule.span R (Set.range v))) : hv.linearCombinationEquiv.symm a✝ = ((LinearEquiv.ofInjective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯) ⋯).toEquiv.trans (LinearEquiv.ofTop (LinearMap.range (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯)) ⋯).toEquiv).invFun a✝

@[simp]

theorem LinearIndependent.linearCombinationEquiv_apply_coe {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (l : ι →₀ R) : ↑(hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l

def LinearIndependent.repr {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : ↥(Submodule.span R (Set.range v)) →ₗ[R] ι →₀ R

Linear combination representing a vector in the span of linearly independent vectors.

Given a family of linearly independent vectors, we can represent any vector in their span as a linear combination of these vectors. These are provided by this linear map. It is simply one direction of LinearIndependent.linearCombinationEquiv.

Equations

• hv.repr = ↑hv.linearCombinationEquiv.symm

@[simp]

theorem LinearIndependent.linearCombination_repr {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (x : ↥(Submodule.span R (Set.range v))) : (Finsupp.linearCombination R v) (hv.repr x) = ↑x

theorem LinearIndependent.linearCombination_comp_repr {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : Finsupp.linearCombination R v ∘ₗ hv.repr = (Submodule.span R (Set.range v)).subtype

theorem LinearIndependent.repr_ker {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : LinearMap.ker hv.repr = ⊥

theorem LinearIndependent.repr_range {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : LinearMap.range hv.repr = ⊤

theorem LinearIndependent.repr_eq {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) {l : ι →₀ R} {x : ↥(Submodule.span R (Set.range v))} (eq : (Finsupp.linearCombination R v) l = ↑x) : hv.repr x = l

theorem LinearIndependent.repr_eq_single {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (i : ι) (x : ↥(Submodule.span R (Set.range v))) (hx : ↑x = v i) : hv.repr x = Finsupp.single i 1

theorem LinearIndependent.span_repr_eq {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) [Nontrivial R] (x : ↥(Submodule.span R (Set.range v))) : Span.repr R (Set.range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)

theorem LinearIndependent.not_smul_mem_span {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (i : ι) (a : R) (ha : a • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))) : a = 0

def LinearIndependent.Maximal {ι : Type w} {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {v : ι → M} (_i : LinearIndependent R v) : Prop

A linearly independent family is maximal if there is no strictly larger linearly independent family.

Equations

• _i.Maximal = ∀ (s : Set M), LinearIndependent R Subtype.val → Set.range v ≤ s → Set.range v = s

theorem LinearIndependent.maximal_iff {ι : Type w} {R : Type u} [Semiring R] [Nontrivial R] {M : Type v} [AddCommMonoid M] [Module R M] {v : ι → M} (i : LinearIndependent R v) : i.Maximal ↔ ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Function.Surjective j

An alternative characterization of a maximal linearly independent family, quantifying over types (in the same universe as M) into which the indexing family injects.

theorem linearIndependent_iff_ker {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndependent R v ↔ LinearMap.ker (Finsupp.linearCombination R v) = ⊥

theorem linearIndependent_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0

theorem linearIndependent_iff' {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

theorem linearIndependent_iff'' {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0

theorem not_linearIndependent_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : ¬LinearIndependent R v ↔ ∃ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

theorem Fintype.linearIndependent_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] [Fintype ι] : LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0

theorem Fintype.not_linearIndependent_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] [Fintype ι] : ¬LinearIndependent R v ↔ ∃ (g : ι → R), ∑ i : ι, g i • v i = 0 ∧ ∃ (i : ι), g i ≠ 0

theorem LinearMap.linearIndependent_iff_of_disjoint {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (hf_inj : Disjoint (Submodule.span R (Set.range v)) (ker f)) : LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v

If the kernel of a linear map is disjoint from the span of a family of vectors, then the family is linearly independent iff it is linearly independent after composing with the linear map.

The following give equivalent versions of LinearIndepOn and its negation.

theorem linearIndepOn_iff {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0

@[deprecated linearIndepOn_iff (since := "2025-02-15")]

theorem linearIndependent_comp_subtype {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0

Alias of linearIndepOn_iff.

@[deprecated linearIndepOn_iff (since := "2025-02-15")]

theorem linearIndependent_subtype {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0

Alias of linearIndepOn_iff.

theorem linearDepOn_iff' {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = 0 ∧ f ≠ 0

An indexed set of vectors is linearly dependent iff there is a nontrivial Finsupp.linearCombination of the vectors that is zero.

@[deprecated linearDepOn_iff' (since := "2025-02-15")]

theorem linearDependent_comp_subtype' {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = 0 ∧ f ≠ 0

Alias of linearDepOn_iff'.

---

An indexed set of vectors is linearly dependent iff there is a nontrivial Finsupp.linearCombination of the vectors that is zero.

theorem linearDepOn_iff {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0

A version of linearDepOn_iff' with Finsupp.linearCombination unfolded.

@[deprecated linearDepOn_iff (since := "2025-02-15")]

theorem linearDependent_comp_subtype {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0

Alias of linearDepOn_iff.

---

A version of linearDepOn_iff' with Finsupp.linearCombination unfolded.

theorem linearIndepOn_iff_disjoint {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))

@[deprecated linearIndepOn_iff_disjoint (since := "2025-02-15")]

theorem linearIndependent_comp_subtype_disjoint {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))

Alias of linearIndepOn_iff_disjoint.

@[deprecated linearIndepOn_iff_disjoint (since := "2025-02-15")]

theorem linearIndependent_subtype_disjoint {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))

Alias of linearIndepOn_iff_disjoint.

theorem linearIndepOn_iff_linearCombinationOn {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ LinearMap.ker (Finsupp.linearCombinationOn ι M R v s) = ⊥

@[deprecated linearIndepOn_iff_linearCombinationOn (since := "2025-02-15")]

theorem linearIndependent_iff_linearCombinationOn {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ LinearMap.ker (Finsupp.linearCombinationOn ι M R v s) = ⊥

Alias of linearIndepOn_iff_linearCombinationOn.

Properties which require Ring R

theorem linearIndependent_iff_not_smul_mem_span {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndependent R v ↔ ∀ (i : ι) (a : R), a • v i ∈ Submodule.span R (v '' (Set.univ \ {i})) → a = 0

Properties which require DivisionRing K

These can be considered generalizations of properties of linear independence in vector spaces.

theorem linearIndependent_iff_not_mem_span {ι : Type u'} {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {v : ι → V} : LinearIndependent K v ↔ ∀ (i : ι), v i ∉ Submodule.span K (v '' (Set.univ \ {i}))