# Linear independence #

This file collects basic consequences of linear (in)dependence and includes specialized tests for specific families of vectors.

## Main statements #

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

- `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_sum`: type-specific test for linear independence of families of vector fields;
- `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.

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

source
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`.

See also `LinearIndependent.restrict_scalars'` for a version with more convenient typeclass assumptions.

TODO : `LinearIndepOn` version.

source
theorem LinearIndependent.restrict_scalars' {ι : Type u'} (R : Type u_2) {K : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring K] [SMulWithZero R K] [Module K M] [IsScalarTower R K M] [FaithfulSMul R K] [IsScalarTower R K K] {v : ι → M} (li : LinearIndependent K v) :
LinearIndependent R v
source
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.

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

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

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

source
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
source
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
source
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)
source
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)
source
theorem LinearIndepOn_iff_linearIndepOn_image_injOn {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] :
LinearIndepOn R v s ↔ LinearIndepOn R id (v '' s) ∧ Set.InjOn v s
source
theorem linearIndepOn_congr {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {w : ι → M} (h : Set.EqOn v w s) :
LinearIndepOn R v s ↔ LinearIndepOn R w s
source
theorem LinearIndepOn.congr {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] {w : ι → M} (hli : LinearIndepOn R v s) (h : Set.EqOn v w s) :
LinearIndepOn R w s
source
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] [MulAction G R] [SMul G M] [IsScalarTower G R M] [SMulCommClass G R M] {v : ι → M} (hv : LinearIndependent R v) (w : ι → G) :
LinearIndependent R (w • v)
source
@[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] [MulAction G R] [MulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] (v : ι → M) (w : ι → G) :
LinearIndependent R (w • v) ↔ LinearIndependent R v
source
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)
source
@[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
source
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, ⋯⟩
source
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.

source
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
source
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 `ι`.

source
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))
source
theorem LinearIndependent.notMem_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)
source
@[deprecated LinearIndependent.notMem_span_image (since := "2025-05-23")]
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)

Alias of `LinearIndependent.notMem_span_image`.

source
theorem LinearIndependent.linearCombination_ne_of_notMem_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
source
@[deprecated LinearIndependent.linearCombination_ne_of_notMem_support (since := "2025-05-23")]
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

Alias of `LinearIndependent.linearCombination_ne_of_notMem_support`.

source
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)
source
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
source
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
source
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
source
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
source
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`.

source
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 = ⊥`.

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

source
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'`.

source
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} [Semiring R'] [AddCommMonoid 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'`.

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

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

### Properties which require `Ring R` #

source
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)))
source
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')
source
theorem LinearIndepOn.union {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {t : Set ι} (hs : LinearIndepOn R v s) (ht : LinearIndepOn R v t) (hdj : Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))) :
LinearIndepOn R v (s ∪ t)
source
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) (hdj : Disjoint (Submodule.span R s) (Submodule.span R t)) :
LinearIndepOn R id (s ∪ t)
source
theorem linearIndepOn_union_iff {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {t : Set ι} (hdj : Disjoint s t) :
LinearIndepOn R v (s ∪ t) ↔ LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
source
theorem linearIndepOn_id_union_iff {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {s t : Set M} (hdj : Disjoint s t) :
LinearIndepOn R id (s ∪ t) ↔ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (Submodule.span R s) (Submodule.span R t)
source
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)
source
theorem linearIndependent_monoidHom (G : Type u_6) [MulOneClass G] (L : Type u_7) [CommRing L] [NoZeroDivisors L] :
LinearIndependent L fun (f : G →* L) => ⇑f

Dedekind's linear independence of characters

source
theorem linearIndependent_unique_iff {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] {v : ι → M} [Unique ι] :
LinearIndependent R v ↔ v default ≠ 0
source
@[deprecated LinearIndependent.of_subsingleton (since := "2025-11-11")]
theorem linearIndependent_unique {ι : Type u'} {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] {v : ι → M} [Unique ι] :
v default ≠ 0 → LinearIndependent R v

Alias of the reverse direction of `linearIndependent_unique_iff`.

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