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

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.

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

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

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)

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)

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

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

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

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)

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

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

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

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

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

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

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

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.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} [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'.

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.

Properties which require Ring R

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

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)

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

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)

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)

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

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.

@[simp]

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

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] {i : ι} {v : ι → M} : v i ≠ 0 → LinearIndepOn R v {i}

Alias of the reverse direction of linearIndepOn_singleton_iff.

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}

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