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. Then we 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.

Main statements

We prove several specialized tests for linear independence of families of vectors and of sets of vectors.

• 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 ι;
• linearIndependent_empty_type: a family indexed by an empty type is linearly independent;
• linearIndependent_unique_iff: if ι is a singleton, then LinearIndependent K v is equivalent to v default ≠ 0;
• linearIndependent_option, linearIndependent_sum, linearIndependent_fin_cons, linearIndependent_fin_succ: type-specific tests for linear independence of families of vector fields;
• linearIndependent_insert, linearIndependent_union, linearIndependent_pair, linearIndependent_singleton: linear independence tests for set operations.

In many cases we additionally provide dot-style operations (e.g., LinearIndependent.union) to make the linear independence tests usable as hv.insert ha etc.

We also prove that, when working over a division ring, any family of vectors includes a linear independent subfamily spanning the same subspace.

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 reason about linear independence of the of a subfamily of an indexed family v : ι → M of vectors corresponding to a set s : Set ι, then use LinearIndepOn R v s. If s : Set M is instead an explicit set of vectors, then use LinearIndepOn R id s.

The lemmas LinearIndepOn.linearIndependent and linearIndepOn_id_range_iff 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.restrict_scalars {ι : Type u'} {R : Type u_2} {K : Type u_3} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring K] [SMulWithZero R K] [Module K M] [IsScalarTower R K M] (hinj : Function.Injective fun (r : R) => r • 1) (li : LinearIndependent K v) : LinearIndependent R v

A set of linearly independent vectors in a module M over a semiring K is also linearly independent over a subring R of K. The implementation uses minimal assumptions about the relationship between R, K and M. The version where K is an R-algebra is LinearIndependent.restrict_scalars_algebras. TODO : LinearIndepOn version.

@[deprecated linearIndependent_iff_injective_linearCombination (since := "2024-08-29")]

theorem linearIndependent_iff_injective_total {ι : 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 linearIndependent_iff_injective_linearCombination.

@[deprecated LinearIndependent.injective_linearCombination (since := "2024-08-29")]

theorem LinearIndependent.injective_total {ι : 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.

---

Alias of the forward direction of linearIndependent_iff_injective_linearCombination.

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.linearIndependent_iff'ₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] : LinearIndependent R v ↔ Function.Injective ⇑((LinearMap.lsum R (fun (x : ι) => R) ℕ) fun (i : ι) => LinearMap.id.smulRight (v i))

A finite family of vectors v i is linear independent iff the linear map that sends c : ι → R to ∑ i, c i • v i is injective.

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.pair_iffₛ {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x y : M} : LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

theorem LinearIndependent.eq_of_pair {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x y : M} (h : LinearIndependent R ![x, y]) {s t s' t' : R} (h' : s • x + t • y = s' • x + t' • y) : s = s' ∧ t = t'

theorem LinearIndependent.eq_zero_of_pair' {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x y : M} (h : LinearIndependent R ![x, y]) {s t : R} (h' : s • x = t • y) : s = 0 ∧ t = 0

theorem LinearIndependent.eq_zero_of_pair {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x y : M} (h : LinearIndependent R ![x, y]) {s t : R} (h' : s • x + t • y = 0) : s = 0 ∧ t = 0

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 Submodule.range_ker_disjoint {ι : 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'} (hv : LinearIndependent R (⇑f ∘ v)) : Disjoint (span R (Set.range v)) (LinearMap.ker f)

If v is an injective family of vectors such that f ∘ v is linearly independent, then v spans a submodule disjoint from the kernel of f. TODO : LinearIndepOn version.

theorem LinearIndependent.map_of_injective_injectiveₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {R' : Type u_6} {M' : Type u_7} [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v) (i : R' → R) (j : M →+ M') (hi : Function.Injective i) (hj : Function.Injective ⇑j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : LinearIndependent R' (⇑j ∘ v)

If M / R and M' / R' are modules, i : R' → R is a map, j : M →+ M' is a monoid map, such that they are both injective, and compatible with the scalar multiplications on M and M', then j sends linearly independent families of vectors to linearly independent families of vectors. As a special case, taking R = R' it is LinearIndependent.map_injOn. TODO : LinearIndepOn version.

theorem LinearIndependent.map_of_surjective_injectiveₛ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {R' : Type u_6} {M' : Type u_7} [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v) (i : R → R') (j : M →+ M') (hi : Function.Surjective i) (hj : Function.Injective ⇑j) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (⇑j ∘ v)

If M / R and M' / R' are modules, i : R → R' is a surjective map, and j : M →+ M' is an injective monoid map, such that the scalar multiplications on M and M' are compatible, then j sends linearly independent families of vectors to linearly independent families of vectors. As a special case, taking R = R' it is LinearIndependent.map_injOn. TODO : LinearIndepOn version.

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.map_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'] (hv : LinearIndependent R v) (f : M →ₗ[R] M') (hf_inj : Set.InjOn ⇑f ↑(Submodule.span R (Set.range v))) : LinearIndependent R (⇑f ∘ v)

If a linear map is injective on the span of a family of linearly independent vectors, then the family stays linearly independent after composing with the linear map. See LinearIndependent.map for the version with Set.InjOn replaced by Disjoint when working over a ring.

theorem LinearIndepOn.map_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'] (hv : LinearIndepOn R v s) (f : M →ₗ[R] M') (hf_inj : Set.InjOn ⇑f ↑(Submodule.span R (v '' s))) : LinearIndepOn R (⇑f ∘ 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.comp_of_image {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set ι'} {f : ι' → ι} (h : LinearIndepOn R v (f '' s)) (hf : Set.InjOn f s) : LinearIndepOn R (v ∘ f) s

@[deprecated LinearIndepOn.comp_of_image (since := "2025-02-14")]

theorem LinearIndependent.comp_of_image {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set ι'} {f : ι' → ι} (h : LinearIndepOn R v (f '' s)) (hf : Set.InjOn f s) : LinearIndepOn R (v ∘ f) s

Alias of LinearIndepOn.comp_of_image.

theorem LinearIndepOn.image_of_comp {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {s : Set ι} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f : ι → ι') (g : ι' → M) (hs : LinearIndepOn R (g ∘ f) s) : LinearIndepOn R g (f '' s)

@[deprecated LinearIndepOn.image_of_comp (since := "2025-02-14")]

theorem LinearIndependent.image_of_comp {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {s : Set ι} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f : ι → ι') (g : ι' → M) (hs : LinearIndepOn R (g ∘ f) s) : LinearIndepOn R g (f '' s)

Alias of LinearIndepOn.image_of_comp.

theorem LinearIndepOn.id_image {ι : 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) : LinearIndepOn R id (v '' s)

@[deprecated LinearIndepOn.id_image (since := "2025-02-14")]

theorem LinearIndependent.image {ι : 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) : LinearIndepOn R id (v '' s)

Alias of LinearIndepOn.id_image.

theorem LinearIndependent.group_smul {ι : Type u'} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_6} [hG : Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] {v : ι → M} (hv : LinearIndependent R v) (w : ι → G) : LinearIndependent R (w • v)

@[simp]

theorem LinearIndependent.group_smul_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_6} [hG : Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] (v : ι → M) (w : ι → G) : LinearIndependent R (w • v) ↔ LinearIndependent R v

theorem LinearIndependent.units_smul {ι : Type u'} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hv : LinearIndependent R v) (w : ι → Rˣ) : LinearIndependent R (w • v)

@[simp]

theorem LinearIndependent.units_smul_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (v : ι → M) (w : ι → Rˣ) : LinearIndependent R (w • v) ↔ LinearIndependent R v

theorem linearIndependent_span {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hs : LinearIndependent R v) : LinearIndependent R fun (i : ι) => ⟨v i, ⋯⟩

theorem linearIndependent_finset_map_embedding_subtype {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (li : LinearIndependent R Subtype.val) (t : Finset ↑s) : LinearIndependent R Subtype.val

Every finite subset of a linearly independent set is linearly independent.

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ₛ.

theorem LinearIndepOn.mono {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {t s : Set ι} (hs : LinearIndepOn R v s) (h : t ⊆ s) : LinearIndepOn R v t

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

theorem LinearIndependent.mono {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {t s : Set ι} (hs : LinearIndepOn R v s) (h : t ⊆ s) : LinearIndepOn R v t

Alias of LinearIndepOn.mono.

theorem linearIndepOn_of_finite {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set ι) (H : ∀ t ⊆ s, t.Finite → LinearIndepOn R v t) : LinearIndepOn R v s

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

theorem linearIndependent_of_finite {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set ι) (H : ∀ t ⊆ s, t.Finite → LinearIndepOn R v t) : LinearIndepOn R v s

Alias of linearIndepOn_of_finite.

theorem linearIndepOn_iUnion_of_directed {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {η : Type u_6} {s : η → Set ι} (hs : Directed (fun (x1 x2 : Set ι) => x1 ⊆ x2) s) (h : ∀ (i : η), LinearIndepOn R v (s i)) : LinearIndepOn R v (⋃ (i : η), s i)

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

theorem linearIndependent_iUnion_of_directed {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {η : Type u_6} {s : η → Set ι} (hs : Directed (fun (x1 x2 : Set ι) => x1 ⊆ x2) s) (h : ∀ (i : η), LinearIndepOn R v (s i)) : LinearIndepOn R v (⋃ (i : η), s i)

Alias of linearIndepOn_iUnion_of_directed.

theorem linearIndepOn_sUnion_of_directed {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Set ι)} (hs : DirectedOn (fun (x1 x2 : Set ι) => x1 ⊆ x2) s) (h : ∀ a ∈ s, LinearIndepOn R v a) : LinearIndepOn R v (⋃₀ s)

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

theorem linearIndependent_sUnion_of_directed {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Set ι)} (hs : DirectedOn (fun (x1 x2 : Set ι) => x1 ⊆ x2) s) (h : ∀ a ∈ s, LinearIndepOn R v a) : LinearIndepOn R v (⋃₀ s)

Alias of linearIndepOn_sUnion_of_directed.

theorem linearIndepOn_biUnion_of_directed {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {η : Type u_6} {s : Set η} {t : η → Set ι} (hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) => x1 ⊆ x2) s) (h : ∀ a ∈ s, LinearIndepOn R v (t a)) : LinearIndepOn R v (⋃ a ∈ s, t a)

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

theorem linearIndependent_biUnion_of_directed {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {η : Type u_6} {s : Set η} {t : η → Set ι} (hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) => x1 ⊆ x2) s) (h : ∀ a ∈ s, LinearIndepOn R v (t a)) : LinearIndepOn R v (⋃ a ∈ s, t a)

Alias of linearIndepOn_biUnion_of_directed.

theorem LinearIndependent.eq_of_smul_apply_eq_smul_apply {ι : Type u'} {R : Type u_2} [Semiring R] {M : Type u_6} [AddCommMonoid M] [Module R M] {v : ι → M} (li : LinearIndependent R v) (c d : R) (i j : ι) (hc : c ≠ 0) (h : c • v i = d • v j) : i = j

Linear independent families are injective, even if you multiply either side.

The following lemmas use the subtype defined by a set in M as the index set ι.

theorem LinearIndependent.disjoint_span_image {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) {s t : Set ι} (hs : Disjoint s t) : Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))

theorem LinearIndependent.not_mem_span_image {ι : 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) {s : Set ι} {x : ι} (h : x ∉ s) : v x ∉ Submodule.span R (v '' s)

theorem LinearIndependent.linearCombination_ne_of_not_mem_support {ι : 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) {x : ι} (f : ι →₀ R) (h : x ∉ f.support) : (Finsupp.linearCombination R v) f ≠ v x

@[deprecated LinearIndependent.linearCombination_ne_of_not_mem_support (since := "2024-08-29")]

theorem LinearIndependent.total_ne_of_not_mem_support {ι : 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) {x : ι} (f : ι →₀ R) (h : x ∉ f.support) : (Finsupp.linearCombination R v) f ≠ v x

Alias of LinearIndependent.linearCombination_ne_of_not_mem_support.

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✝

@[deprecated LinearIndependent.linearCombinationEquiv (since := "2024-08-29")]

def LinearIndependent.totalEquiv {ι : 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))

Alias of LinearIndependent.linearCombinationEquiv.

---

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

Equations

• @LinearIndependent.totalEquiv = @LinearIndependent.linearCombinationEquiv

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

@[deprecated LinearIndependent.linearCombinationEquiv_apply_coe (since := "2024-08-29")]

theorem LinearIndependent.totalEquiv_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

Alias of LinearIndependent.linearCombinationEquiv_apply_coe.

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

@[deprecated LinearIndependent.linearCombination_repr (since := "2024-08-29")]

theorem LinearIndependent.total_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

Alias of LinearIndependent.linearCombination_repr.

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

@[deprecated LinearIndependent.linearCombination_comp_repr (since := "2024-08-29")]

theorem LinearIndependent.total_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

Alias of LinearIndependent.linearCombination_comp_repr.

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

theorem LinearIndependent.iSupIndep_span_singleton {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : iSupIndep fun (i : ι) => Submodule.span R {v i}

See also iSupIndep_iff_linearIndependent_of_ne_zero.

@[deprecated LinearIndependent.iSupIndep_span_singleton (since := "2024-11-24")]

theorem LinearIndependent.independent_span_singleton {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : iSupIndep fun (i : ι) => Submodule.span R {v i}

Alias of LinearIndependent.iSupIndep_span_singleton.

---

See also iSupIndep_iff_linearIndependent_of_ne_zero.

theorem LinearIndepOn.id_imageₛ {R : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s) (hf_inj : Set.InjOn ⇑f ↑(Submodule.span R s)) : LinearIndepOn R id (⇑f '' s)

@[deprecated LinearIndepOn.id_imageₛ (since := "2025-02-14")]

theorem LinearIndependent.image_subtypeₛ {R : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s) (hf_inj : Set.InjOn ⇑f ↑(Submodule.span R s)) : LinearIndepOn R id (⇑f '' s)

Alias of LinearIndepOn.id_imageₛ.

theorem linearIndependent_inl_union_inr' {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {v : ι → M} {v' : ι' → M'} (hv : LinearIndependent R v) (hv' : LinearIndependent R v') : LinearIndependent R (Sum.elim (⇑(LinearMap.inl R M M') ∘ v) (⇑(LinearMap.inr R M M') ∘ v'))

theorem LinearIndependent.inl_union_inr {R : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {s : Set M} {t : Set M'} (hs : LinearIndependent R fun (x : ↑s) => ↑x) (ht : LinearIndependent R fun (x : ↑t) => ↑x) : LinearIndependent R fun (x : ↑(⇑(LinearMap.inl R M M') '' s ∪ ⇑(LinearMap.inr R M M') '' t)) => ↑x

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 exists_maximal_linearIndepOn' {ι : Type u'} (R : Type u_2) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

TODO : refactor to use Maximal.

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

theorem exists_maximal_independent' {ι : Type u'} (R : Type u_2) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Alias of exists_maximal_linearIndepOn'.

---

TODO : refactor to use Maximal.

theorem surjective_of_linearIndependent_of_span {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (hv : LinearIndependent R v) (f : ι' ↪ ι) (hss : Set.range v ⊆ ↑(Submodule.span R (Set.range (v ∘ ⇑f)))) : Function.Surjective ⇑f

theorem eq_of_linearIndepOn_id_of_span_subtype {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {s t : Set M} (hs : LinearIndepOn R id s) (h : t ⊆ s) (hst : s ⊆ ↑(Submodule.span R t)) : s = t

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

theorem eq_of_linearIndependent_of_span_subtype {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {s t : Set M} (hs : LinearIndepOn R id s) (h : t ⊆ s) (hst : s ⊆ ↑(Submodule.span R t)) : s = t

Alias of eq_of_linearIndepOn_id_of_span_subtype.

theorem le_of_span_le_span {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {s t u : Set M} (hl : LinearIndepOn R id u) (hsu : s ⊆ u) (htu : t ⊆ u) (hst : Submodule.span R s ≤ Submodule.span R t) : s ⊆ t

theorem span_le_span_iff {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {s t u : Set M} (hl : LinearIndependent R Subtype.val) (hsu : s ⊆ u) (htu : t ⊆ u) : Submodule.span R s ≤ Submodule.span R t ↔ s ⊆ t

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.linearIndependent_iff' {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] [Fintype ι] [DecidableEq ι] : LinearIndependent R v ↔ LinearMap.ker ((LinearMap.lsum R (fun (x : ι) => R) ℕ) fun (i : ι) => LinearMap.id.smulRight (v i)) = ⊥

A finite family of vectors v i is linear independent iff the linear map that sends c : ι → R to ∑ i, c i • v i has the trivial kernel.

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 LinearIndependent.pair_iff {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {x y : M} : LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Also see LinearIndependent.pair_iff' for a simpler version over fields.

theorem LinearIndependent.pair_symm_iff {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {x y : M} : LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

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.

theorem LinearIndependent.eq_coords_of_eq {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [Fintype ι] {v : ι → M} (hv : LinearIndependent R v) {f g : ι → R} (heq : ∑ i : ι, f i • v i = ∑ i : ι, g i • v i) (i : ι) : f i = g i

If ∑ i, f i • v i = ∑ i, g i • v i, then for all i, f i = g i.

theorem LinearIndependent.map {ι : 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'] (hv : LinearIndependent R v) {f : M →ₗ[R] M'} (hf_inj : Disjoint (Submodule.span R (Set.range v)) (LinearMap.ker f)) : LinearIndependent R (⇑f ∘ v)

If v is a linearly independent family of vectors and the kernel of a linear map f is disjoint with the submodule spanned by the vectors of v, then f ∘ v is a linearly independent family of vectors. See also LinearIndependent.map' for a special case assuming ker f = ⊥.

theorem LinearIndependent.map' {ι : 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'] (hv : LinearIndependent R v) (f : M →ₗ[R] M') (hf_inj : LinearMap.ker f = ⊥) : LinearIndependent R (⇑f ∘ v)

An injective linear map sends linearly independent families of vectors to linearly independent families of vectors. See also LinearIndependent.map for a more general statement.

theorem LinearIndependent.map_of_injective_injective {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {R' : Type u_6} {M' : Type u_7} [Ring R'] [AddCommGroup M'] [Module R' M'] (hv : LinearIndependent R v) (i : R' → R) (j : M →+ M') (hi : ∀ (r : R'), i r = 0 → r = 0) (hj : ∀ (m : M), j m = 0 → m = 0) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : LinearIndependent R' (⇑j ∘ v)

If M / R and M' / R' are modules, i : R' → R is a map, j : M →+ M' is a monoid map, such that they send non-zero elements to non-zero elements, and compatible with the scalar multiplications on M and M', then j sends linearly independent families of vectors to linearly independent families of vectors. As a special case, taking R = R' it is LinearIndependent.map'.

theorem LinearIndependent.map_of_surjective_injective {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {R' : Type u_6} {M' : Type u_7} [Ring R'] [AddCommGroup M'] [Module R' M'] (hv : LinearIndependent R v) (i : R → R') (j : M →+ M') (hi : Function.Surjective i) (hj : ∀ (m : M), j m = 0 → m = 0) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (⇑j ∘ v)

If M / R and M' / R' are modules, i : R → R' is a surjective map which maps zero to zero, j : M →+ M' is a monoid map which sends non-zero elements to non-zero elements, such that the scalar multiplications on M and M' are compatible, then j sends linearly independent families of vectors to linearly independent families of vectors. As a special case, taking R = R' it is LinearIndependent.map'.

theorem LinearMap.linearIndependent_iff {ι : 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 : ker f = ⊥) : LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v

If f is an injective linear map, then the family f ∘ v is linearly independent if and only if the family v is linearly independent.

theorem LinearIndependent.fin_cons' {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ} (x : M) (v : Fin m → M) (hli : LinearIndependent R v) (x_ortho : ∀ (c : R) (y : ↥(Submodule.span R (Set.range v))), c • x + ↑y = 0 → c = 0) : LinearIndependent R (Fin.cons x v)

See LinearIndependent.fin_cons for a family of elements in a vector space.

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 := "2024-08-29")]

theorem linearIndependent_iff_totalOn {ι : 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.

@[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.linear_combination_pair_of_det_ne_zero {R : Type u_6} {M : Type u_7} [CommRing R] [NoZeroDivisors R] [AddCommGroup M] [Module R M] {x y : M} (h : LinearIndependent R ![x, y]) {a b c d : R} (h' : a * d - b * c ≠ 0) : LinearIndependent R ![a • x + b • y, c • x + d • y]

If two vectors x and y are linearly independent, so are their linear combinations a x + b y and c x + d y provided the determinant a * d - b * c is nonzero.

theorem linearIndependent_sum {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {v : ι ⊕ ι' → M} : LinearIndependent R v ↔ LinearIndependent R (v ∘ Sum.inl) ∧ LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (Submodule.span R (Set.range (v ∘ Sum.inl))) (Submodule.span R (Set.range (v ∘ Sum.inr)))

theorem LinearIndependent.sum_type {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {v' : ι' → M} (hv : LinearIndependent R v) (hv' : LinearIndependent R v') (h : Disjoint (Submodule.span R (Set.range v)) (Submodule.span R (Set.range v'))) : LinearIndependent R (Sum.elim v v')

theorem LinearIndepOn.id_union {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {s t : Set M} (hs : LinearIndepOn R id s) (ht : LinearIndepOn R id t) (hst : Disjoint (Submodule.span R s) (Submodule.span R t)) : LinearIndepOn R id (s ∪ t)

@[deprecated LinearIndepOn.id_union (since := "2025-02-14")]

theorem LinearIndependent.union {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {s t : Set M} (hs : LinearIndepOn R id s) (ht : LinearIndepOn R id t) (hst : Disjoint (Submodule.span R s) (Submodule.span R t)) : LinearIndepOn R id (s ∪ t)

Alias of LinearIndepOn.id_union.

theorem linearIndepOn_id_iUnion_finite {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {f : ι → Set M} (hl : ∀ (i : ι), LinearIndepOn R id (f i)) (hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i))) : LinearIndepOn R id (⋃ (i : ι), f i)

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

theorem linearIndependent_iUnion_finite_subtype {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {f : ι → Set M} (hl : ∀ (i : ι), LinearIndepOn R id (f i)) (hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i))) : LinearIndepOn R id (⋃ (i : ι), f i)

Alias of linearIndepOn_id_iUnion_finite.

theorem linearIndependent_iUnion_finite {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {η : Type u_6} {ιs : η → Type u_7} {f : (j : η) → ιs j → M} (hindep : ∀ (j : η), LinearIndependent R (f j)) (hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (Submodule.span R (Set.range (f i))) (⨆ i ∈ t, Submodule.span R (Set.range (f i)))) : LinearIndependent R fun (ji : (j : η) × ιs j) => f ji.fst ji.snd

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

theorem exists_maximal_linearIndepOn {ι : Type u'} (R : Type u_2) {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (v : ι → M) : ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ a • v i ∈ Submodule.span R (v '' s)

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

theorem exists_maximal_independent {ι : Type u'} (R : Type u_2) {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (v : ι → M) : ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ a • v i ∈ Submodule.span R (v '' s)

Alias of exists_maximal_linearIndepOn.

theorem LinearIndepOn.image {R : Type u_2} {M : Type u_4} {M' : Type u_5} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s) (hf_inj : Disjoint (Submodule.span R s) (LinearMap.ker f)) : LinearIndepOn R id (⇑f '' s)

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

theorem LinearIndependent.image_subtype {R : Type u_2} {M : Type u_4} {M' : Type u_5} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s) (hf_inj : Disjoint (Submodule.span R s) (LinearMap.ker f)) : LinearIndepOn R id (⇑f '' s)

Alias of LinearIndepOn.image.

theorem linearIndependent_monoidHom (G : Type u_6) [Monoid G] (L : Type u_7) [CommRing L] [NoZeroDivisors L] : LinearIndependent L fun (f : G →* L) => ⇑f

Dedekind's linear independence of characters

Stacks Tag 0CKL

theorem linearIndependent_algHom_toLinearMap (K : Type u_6) (M : Type u_7) (L : Type u_8) [CommSemiring K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] : LinearIndependent L AlgHom.toLinearMap

Stacks Tag 0CKM

theorem linearIndependent_algHom_toLinearMap' (K : Type u_6) (M : Type u_7) (L : Type u_8) [CommRing K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] [NoZeroSMulDivisors K L] : LinearIndependent K AlgHom.toLinearMap

theorem linearIndependent_unique_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (v : ι → M) [Unique ι] : LinearIndependent R v ↔ v default ≠ 0

theorem linearIndependent_unique {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (v : ι → M) [Unique ι] : v default ≠ 0 → LinearIndependent R v

Alias of the reverse direction of linearIndependent_unique_iff.

theorem LinearIndepOn.singleton {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : ι → M} {i : ι} (hi : v i ≠ 0) : LinearIndepOn R v {i}

theorem LinearIndepOn.id_singleton (R : Type u_2) {M : Type u_4} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (hx : x ≠ 0) : LinearIndepOn R id {x}

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

theorem linearIndependent_singleton (R : Type u_2) {M : Type u_4} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (hx : x ≠ 0) : LinearIndepOn R id {x}

Alias of LinearIndepOn.id_singleton.

@[simp]

theorem linearIndependent_subsingleton_index_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Subsingleton ι] (f : ι → M) : LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

@[simp]

theorem linearIndependent_subsingleton_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Subsingleton M] (f : ι → M) : LinearIndependent R f ↔ IsEmpty ι

Properties which require DivisionRing K

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

theorem mem_span_insert_exchange {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x y : V} : x ∈ Submodule.span K (insert y s) → x ∉ Submodule.span K s → y ∈ Submodule.span K (insert x s)

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

theorem LinearIndepOn.insert {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V} (hs : LinearIndepOn K id s) (hx : x ∉ Submodule.span K s) : LinearIndepOn K id (insert x s)

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

theorem LinearIndependent.insert {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V} (hs : LinearIndepOn K id s) (hx : x ∉ Submodule.span K s) : LinearIndepOn K id (Insert.insert x s)

Alias of LinearIndepOn.insert.

theorem linearIndependent_option' {ι : Type u'} {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {v : ι → V} {x : V} : (LinearIndependent K fun (o : Option ι) => o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)

theorem LinearIndependent.option {ι : Type u'} {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {v : ι → V} {x : V} (hv : LinearIndependent K v) (hx : x ∉ Submodule.span K (Set.range v)) : LinearIndependent K fun (o : Option ι) => o.casesOn' x v

theorem linearIndependent_option {ι : Type u'} {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {v : Option ι → V} : LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ Submodule.span K (Set.range (v ∘ some))

theorem linearIndepOn_insert {ι : Type u'} {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set ι} {a : ι} {f : ι → V} (has : a ∉ s) : LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s)

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

theorem linearIndependent_insert' {ι : Type u'} {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set ι} {a : ι} {f : ι → V} (has : a ∉ s) : LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s)

Alias of linearIndepOn_insert.

theorem linearIndepOn_id_insert {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V} (hxs : x ∉ s) : LinearIndepOn K id (insert x s) ↔ LinearIndepOn K id s ∧ x ∉ Submodule.span K s

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

theorem linearIndependent_insert {ι : Type u'} {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set ι} {a : ι} {f : ι → V} (has : a ∉ s) : LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s)

Alias of linearIndepOn_insert.

theorem linearIndepOn_id_pair {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {x y : V} (hx : x ≠ 0) (hy : ∀ (a : K), a • x ≠ y) : LinearIndepOn K id {x, y}

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

theorem linearIndependent_pair {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {x y : V} (hx : x ≠ 0) (hy : ∀ (a : K), a • x ≠ y) : LinearIndepOn K id {x, y}

Alias of linearIndepOn_id_pair.

theorem LinearIndependent.pair_iff' {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {x y : V} (hx : x ≠ 0) : LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y

Also see LinearIndependent.pair_iff for the version over arbitrary rings.

theorem linearIndependent_fin_cons {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {x : V} {n : ℕ} {v : Fin n → V} : LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)

theorem linearIndependent_fin_snoc {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {x : V} {n : ℕ} {v : Fin n → V} : LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)

theorem LinearIndependent.fin_cons {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {x : V} {n : ℕ} {v : Fin n → V} (hv : LinearIndependent K v) (hx : x ∉ Submodule.span K (Set.range v)) : LinearIndependent K (Fin.cons x v)

See LinearIndependent.fin_cons' for an uglier version that works if you only have a module over a semiring.

theorem linearIndependent_fin_succ {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin (n + 1) → V} : LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (Set.range (Fin.tail v))

theorem linearIndependent_fin_succ' {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin (n + 1) → V} : LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ Submodule.span K (Set.range (Fin.init v))

def equiv_linearIndependent {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] (n : ℕ) : { s : Fin (n + 1) → V // LinearIndependent K s } ≃ (s : { s : Fin n → V // LinearIndependent K s }) × ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ

Equivalence between k + 1 vectors of length n and k vectors of length n along with a vector in the complement of their span.

Equations

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

theorem linearIndependent_fin2 {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {f : Fin 2 → V} : LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0

theorem exists_linearIndepOn_id_extension {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : ∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndepOn K id b

TODO : generalize this and related results to non-identity functions

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

theorem exists_linearIndependent_extension {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : ∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndepOn K id b

Alias of exists_linearIndepOn_id_extension.

---

TODO : generalize this and related results to non-identity functions

theorem exists_linearIndependent (K : Type u_3) {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] (t : Set V) : ∃ b ⊆ t, Submodule.span K b = Submodule.span K t ∧ LinearIndependent K Subtype.val

theorem exists_linearIndependent' {ι : Type u'} (K : Type u_3) {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] (v : ι → V) : ∃ (κ : Type u') (a : κ → ι), Function.Injective a ∧ Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧ LinearIndependent K (v ∘ a)

Indexed version of exists_linearIndependent.

noncomputable def LinearIndepOn.extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : Set V

LinearIndepOn.extend adds vectors to a linear independent set s ⊆ t until it spans all elements of t. TODO - generalize the lemmas below to functions that aren't the identity.

Equations

• hs.extend hst = Classical.choose ⋯

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

def LinearIndependent.extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : Set V

Alias of LinearIndepOn.extend.

---

LinearIndepOn.extend adds vectors to a linear independent set s ⊆ t until it spans all elements of t. TODO - generalize the lemmas below to functions that aren't the identity.

Equations

• @LinearIndependent.extend = @LinearIndepOn.extend

theorem LinearIndepOn.extend_subset {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : hs.extend hst ⊆ t

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

theorem LinearIndependent.extend_subset {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : hs.extend hst ⊆ t

Alias of LinearIndepOn.extend_subset.

theorem LinearIndepOn.subset_extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : s ⊆ hs.extend hst

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

theorem LinearIndependent.subset_extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : s ⊆ hs.extend hst

Alias of LinearIndepOn.subset_extend.

theorem LinearIndepOn.subset_span_extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : t ⊆ ↑(Submodule.span K (hs.extend hst))

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

theorem LinearIndependent.subset_span_extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : t ⊆ ↑(Submodule.span K (hs.extend hst))

Alias of LinearIndepOn.subset_span_extend.

theorem LinearIndepOn.span_extend_eq_span {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : Submodule.span K (hs.extend hst) = Submodule.span K t

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

theorem LinearIndependent.span_extend_eq_span {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : Submodule.span K (hs.extend hst) = Submodule.span K t

Alias of LinearIndepOn.span_extend_eq_span.

theorem LinearIndepOn.linearIndepOn_extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : LinearIndepOn K id (hs.extend hst)

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

theorem LinearIndependent.linearIndependent_extend {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : LinearIndepOn K id (hs.extend hst)

Alias of LinearIndepOn.linearIndepOn_extend.

theorem exists_of_linearIndepOn_of_finite_span {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {t : Finset V} (hs : LinearIndepOn K id s) (hst : s ⊆ ↑(Submodule.span K ↑t)) : ∃ (t' : Finset V), ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

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

theorem exists_of_linearIndependent_of_finite_span {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {t : Finset V} (hs : LinearIndepOn K id s) (hst : s ⊆ ↑(Submodule.span K ↑t)) : ∃ (t' : Finset V), ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Alias of exists_of_linearIndepOn_of_finite_span.

theorem exists_finite_card_le_of_finite_of_linearIndependent_of_span {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (ht : t.Finite) (hs : LinearIndepOn K id s) (hst : s ⊆ ↑(Submodule.span K t)) : ∃ (h : s.Finite), h.toFinset.card ≤ ht.toFinset.card