mathlib documentation

linear_algebra.linear_independent

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 linear_independent R v as ker (finsupp.total ι M R v) = ⊥. Here finsupp.total 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 injectivity of finsupp.total ι M 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.

Main statements #

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

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

We also prove that any family of vectors includes a linear independent subfamily spanning the same submodule.

Implementation notes #

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

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

Tags #

linearly dependent, linear dependence, linearly independent, linear independence

def linear_independent {ι : Type u_1} (R : Type u_3) {M : Type u_5} (v : ι → M) [semiring R] [add_comm_monoid M] [module R M] :
Prop

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

Equations
theorem linear_independent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] :
linear_independent R v ∀ (l : ι →₀ R), (finsupp.total ι M R v) l = 0l = 0
theorem linear_independent_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] :
linear_independent R v ∀ (s : finset ι) (g : ι → R), ∑ (i : ι) in s, g i v i = 0∀ (i : ι), i sg i = 0
theorem linear_independent_iff'' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] :
linear_independent R v ∀ (s : finset ι) (g : ι → R), (∀ (i : ι), i sg i = 0)∑ (i : ι) in s, g i v i = 0∀ (i : ι), g i = 0
theorem linear_dependent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] :
¬linear_independent R v ∃ (s : finset ι) (g : ι → R), ∑ (i : ι) in s, g i v i = 0 ∃ (i : ι) (H : i s), g i 0
theorem fintype.linear_independent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] :
linear_independent R v ∀ (g : ι → R), ∑ (i : ι), g i v i = 0∀ (i : ι), g i = 0
theorem fintype.linear_independent_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] :
linear_independent R v ((linear_map.lsum R (λ (i : ι), R) ) (λ (i : ι), linear_map.id.smul_right (v i))).ker =

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 linear_independent_empty_type {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] [is_empty ι] :
theorem linear_independent.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] [nontrivial R] (i : ι) (hv : linear_independent R v) :
v i 0
theorem linear_independent.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] (h : linear_independent R v) (f : ι' → ι) (hf : function.injective f) :

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

theorem linear_independent.map {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (hv : linear_independent R v) {f : M →ₗ[R] M'} (hf_inj : disjoint (submodule.span R (set.range v)) f.ker) :

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

theorem linear_independent.map' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (hv : linear_independent R v) (f : M →ₗ[R] M') (hf_inj : f.ker = ) :

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

theorem linear_independent.of_comp {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') (hfv : linear_independent R (f v)) :

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

theorem linear_map.linear_independent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') (hf_inj : f.ker = ) :

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 linear_independent_of_subsingleton {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] [subsingleton R] :
theorem linear_independent_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (e : ι ι') {f : ι' → M} :
theorem linear_independent_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (e : ι ι') {f : ι' → M} {g : ι → M} (h : f e = g) :
theorem linear_independent_subtype_range {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} {f : ι → M} (hf : function.injective f) :
theorem linear_independent.of_subtype_range {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} {f : ι → M} (hf : function.injective f) :

Alias of linear_independent_subtype_range.

theorem linear_independent_image {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} {s : set ι} {f : ι → M} (hf : set.inj_on f s) :
linear_independent R (λ (x : s), f x) linear_independent R (λ (x : (f '' s)), x)
theorem linear_independent_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] (hs : linear_independent R v) :
linear_independent R (λ (i : ι), v i, _⟩)
theorem linear_independent.fin_cons' {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {m : } (x : M) (v : fin m → M) (hli : linear_independent R v) (x_ortho : ∀ (c : R) (y : (submodule.span R (set.range v))), c x + y = 0c = 0) :

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

theorem linear_independent.restrict_scalars {ι : Type u_1} {R : Type u_3} {K : Type u_4} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] [semiring K] [smul_with_zero R K] [module K M] [is_scalar_tower R K M] (hinj : function.injective (λ (r : R), r 1)) (li : linear_independent K 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 linear_independent.restrict_scalars_algebras.

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

theorem linear_independent_comp_subtype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] {s : set ι} :
linear_independent R (v coe) ∀ (l : ι →₀ R), l finsupp.supported R R s(finsupp.total ι M R v) l = 0l = 0
theorem linear_dependent_comp_subtype' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] {s : set ι} :
¬linear_independent R (v coe) ∃ (f : ι →₀ R), f finsupp.supported R R s (finsupp.total ι M R v) f = 0 f 0
theorem linear_dependent_comp_subtype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] {s : set ι} :
¬linear_independent R (v coe) ∃ (f : ι →₀ R), f finsupp.supported R R s ∑ (i : ι) in f.support, f i v i = 0 f 0

A version of linear_dependent_comp_subtype' with finsupp.total unfolded.

theorem linear_independent_subtype {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
linear_independent R (λ (x : s), x) ∀ (l : M →₀ R), l finsupp.supported R R s(finsupp.total M M R id) l = 0l = 0
theorem linear_independent_comp_subtype_disjoint {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] {s : set ι} :
theorem linear_independent_subtype_disjoint {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
theorem linear_independent_iff_total_on {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
theorem linear_independent.restrict_of_comp_subtype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [module R M] {s : set ι} (hs : linear_independent R (v coe)) :
theorem linear_independent_empty (R : Type u_3) (M : Type u_5) [semiring R] [add_comm_monoid M] [module R M] :
theorem linear_independent.mono {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {t s : set M} (h : t s) :
linear_independent R (λ (x : s), x)linear_independent R (λ (x : t), x)
theorem linear_independent_of_finite {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set M) (H : ∀ (t : set M), t st.finitelinear_independent R (λ (x : t), x)) :
linear_independent R (λ (x : s), x)
theorem linear_independent_Union_of_directed {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {η : Type u_1} {s : η → set M} (hs : directed has_subset.subset s) (h : ∀ (i : η), linear_independent R (λ (x : (s i)), x)) :
linear_independent R (λ (x : ⋃ (i : η), s i), x)
theorem linear_independent_sUnion_of_directed {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {s : set (set M)} (hs : directed_on has_subset.subset s) (h : ∀ (a : set M), a slinear_independent R (λ (x : a), x)) :
theorem linear_independent_bUnion_of_directed {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {η : Type u_1} {s : set η} {t : η → set M} (hs : directed_on (t ⁻¹'o has_subset.subset) s) (h : ∀ (a : η), a slinear_independent R (λ (x : (t a)), x)) :
linear_independent R (λ (x : ⋃ (a : η) (H : a s), t a), x)

Properties which require ring R #

theorem linear_independent_iff_injective_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] :
theorem linear_independent.injective_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] :

Alias of linear_independent_iff_injective_total.

theorem linear_independent.injective {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] [nontrivial R] (hv : linear_independent R v) :
theorem linear_independent.to_subtype_range {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {f : ι → M} (hf : linear_independent R f) :
theorem linear_independent.to_subtype_range' {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {f : ι → M} (hf : linear_independent R f) {t : set M} (ht : set.range f = t) :
theorem linear_independent.image_of_comp {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {ι' : Type u_2} (s : set ι) (f : ι → ι') (g : ι' → M) (hs : linear_independent R (λ (x : s), g (f x))) :
linear_independent R (λ (x : (f '' s)), g x)
theorem linear_independent.image {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {s : set ι} {f : ι → M} (hs : linear_independent R (λ (x : s), f x)) :
linear_independent R (λ (x : (f '' s)), x)
theorem linear_independent.group_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {G : Type u_2} [hG : group G] [distrib_mul_action G R] [distrib_mul_action G M] [is_scalar_tower G R M] [smul_comm_class G R M] {v : ι → M} (hv : linear_independent R v) (w : ι → G) :
theorem linear_independent.units_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : ι → M} (hv : linear_independent R v) (w : ι → units R) :

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

theorem linear_independent.disjoint_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) {s t : set ι} (hs : disjoint s t) :
theorem linear_independent.not_mem_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] [nontrivial R] (hv : linear_independent R v) {s : set ι} {x : ι} (h : x s) :
v x submodule.span R (v '' s)
theorem linear_independent.total_ne_of_not_mem_support {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] [nontrivial R] (hv : linear_independent R v) {x : ι} (f : ι →₀ R) (h : x f.support) :
(finsupp.total ι M R v) f v x
theorem linear_independent_sum {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : ι ι' → M} :
theorem linear_independent.sum_type {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] {v' : ι' → M} (hv : linear_independent R v) (hv' : linear_independent R v') (h : disjoint (submodule.span R (set.range v)) (submodule.span R (set.range v'))) :
theorem linear_independent.union {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {s t : set M} (hs : linear_independent R (λ (x : s), x)) (ht : linear_independent R (λ (x : t), x)) (hst : disjoint (submodule.span R s) (submodule.span R t)) :
linear_independent R (λ (x : (s t)), x)
theorem linear_independent_Union_finite_subtype {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {f : ι → set M} (hl : ∀ (i : ι), linear_independent R (λ (x : (f i)), x)) (hd : ∀ (i : ι) (t : set ι), t.finitei tdisjoint (submodule.span R (f i)) (⨆ (i : ι) (H : i t), submodule.span R (f i))) :
linear_independent R (λ (x : ⋃ (i : ι), f i), x)
theorem linear_independent_Union_finite {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {η : Type u_1} {ιs : η → Type u_2} {f : Π (j : η), ιs j → M} (hindep : ∀ (j : η), linear_independent R (f j)) (hd : ∀ (i : η) (t : set η), t.finitei tdisjoint (submodule.span R (set.range (f i))) (⨆ (i : η) (H : i t), submodule.span R (set.range (f i)))) :
linear_independent R (λ (ji : Σ (j : η), ιs j), f ji.fst ji.snd)
@[simp]
theorem linear_independent.total_equiv_apply_coe {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) (ᾰ : ι →₀ R) :
((hv.total_equiv) ᾰ) = (finsupp.total ι M R v)
def linear_independent.total_equiv {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) :

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

Equations
@[simp]
theorem linear_independent.total_equiv_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) (ᾰ : (submodule.span R (set.range v))) :
(hv.total_equiv.symm) ᾰ = ((linear_equiv.of_injective (linear_map.cod_restrict (submodule.span R (set.range v)) (finsupp.total ι M R v) linear_independent.total_equiv._proof_1) _).to_equiv.symm) (((linear_equiv.of_top (linear_map.cod_restrict (submodule.span R (set.range v)) (finsupp.total ι M R v) linear_independent.total_equiv._proof_1).range linear_independent.total_equiv._proof_3).to_equiv.symm) ᾰ)
def linear_independent.repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) :

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

Equations
@[simp]
theorem linear_independent.total_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) (x : (submodule.span R (set.range v))) :
(finsupp.total ι M R v) ((hv.repr) x) = x
theorem linear_independent.total_comp_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) :
theorem linear_independent.repr_ker {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) :
theorem linear_independent.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) :
theorem linear_independent.repr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) {l : ι →₀ R} {x : (submodule.span R (set.range v))} (eq : (finsupp.total ι M R v) l = x) :
(hv.repr) x = l
theorem linear_independent.repr_eq_single {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) (i : ι) (x : (submodule.span R (set.range v))) (hx : x = v i) :
theorem linear_independent.span_repr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) [nontrivial R] (x : (submodule.span R (set.range v))) :
theorem linear_independent_iff_not_smul_mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] :
linear_independent R v ∀ (i : ι) (a : R), a v i submodule.span R (v '' (set.univ \ {i}))a = 0
theorem exists_maximal_independent' {ι : Type u_1} (R : Type u_3) {M : Type u_5} [ring R] [add_comm_group M] [module R M] (s : ι → M) :
∃ (I : set ι), linear_independent R (λ (x : I), s x) ∀ (J : set ι), I Jlinear_independent R (λ (x : J), s x)I = J
theorem exists_maximal_independent {ι : Type u_1} (R : Type u_3) {M : Type u_5} [ring R] [add_comm_group M] [module R M] (s : ι → M) :
∃ (I : set ι), linear_independent R (λ (x : I), s x) ∀ (i : ι), i I(∃ (a : R), a 0 a s i submodule.span R (s '' I))
theorem surjective_of_linear_independent_of_span {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] [nontrivial R] (hv : linear_independent R v) (f : ι' ι) (hss : set.range v (submodule.span R (set.range (v f)))) :
theorem eq_of_linear_independent_of_span_subtype {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] [nontrivial R] {s t : set M} (hs : linear_independent R (λ (x : s), x)) (h : t s) (hst : s (submodule.span R t)) :
s = t
theorem linear_independent.image_subtype {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M] [add_comm_group M'] [module R M] [module R M'] {s : set M} {f : M →ₗ[R] M'} (hs : linear_independent R (λ (x : s), x)) (hf_inj : disjoint (submodule.span R s) f.ker) :
linear_independent R (λ (x : (f '' s)), x)
theorem linear_independent.inl_union_inr {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M] [add_comm_group M'] [module R M] [module R M'] {s : set M} {t : set M'} (hs : linear_independent R (λ (x : s), x)) (ht : linear_independent R (λ (x : t), x)) :
linear_independent R (λ (x : ((linear_map.inl R M M') '' s (linear_map.inr R M M') '' t)), x)
theorem linear_independent_inl_union_inr' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ring R] [add_comm_group M] [add_comm_group M'] [module R M] [module R M'] {v : ι → M} {v' : ι' → M'} (hv : linear_independent R v) (hv' : linear_independent R v') :
theorem linear_independent_monoid_hom (G : Type u_1) [monoid G] (L : Type u_2) [comm_ring L] [no_zero_divisors L] :
linear_independent L (λ (f : G →* L), f)

Dedekind's linear independence of characters

theorem le_of_span_le_span {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] [nontrivial R] {s t u : set M} (hl : linear_independent R coe) (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_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] [nontrivial R] {s t u : set M} (hl : linear_independent R coe) (hsu : s u) (htu : t u) :
theorem linear_independent_unique_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [nontrivial R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (v : ι → M) [unique ι] :
theorem linear_independent_unique {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [nontrivial R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (v : ι → M) [unique ι] :
v (default ι) 0linear_independent R v

Alias of linear_independent_unique_iff.

theorem linear_independent_singleton {R : Type u_3} {M : Type u_5} [ring R] [nontrivial R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {x : M} (hx : x 0) :
linear_independent R (λ (x_1 : {x}), x_1)

Properties which require division_ring K #

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

theorem mem_span_insert_exchange {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} {x y : V} :
theorem linear_independent_iff_not_mem_span {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {v : ι → V} :
linear_independent K v ∀ (i : ι), v i submodule.span K (v '' (set.univ \ {i}))
theorem linear_independent.insert {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} {x : V} (hs : linear_independent K (λ (b : s), b)) (hx : x submodule.span K s) :
linear_independent K (λ (b : (insert x s)), b)
theorem linear_independent_option' {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {v : ι → V} {x : V} :
theorem linear_independent.option {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {v : ι → V} {x : V} (hv : linear_independent K v) (hx : x submodule.span K (set.range v)) :
linear_independent K (λ (o : option ι), o.cases_on' x v)
theorem linear_independent_option {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {v : option ι → V} :
theorem linear_independent_insert' {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} {s : set ι} {a : ι} {f : ι → V} (has : a s) :
linear_independent K (λ (x : (insert a s)), f x) linear_independent K (λ (x : s), f x) f a submodule.span K (f '' s)
theorem linear_independent_insert {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} {x : V} (hxs : x s) :
linear_independent K (λ (b : (insert x s)), b) linear_independent K (λ (b : s), b) x submodule.span K s
theorem linear_independent_pair {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {x y : V} (hx : x 0) (hy : ∀ (a : K), a x y) :
theorem linear_independent_fin_cons {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {x : V} {n : } {v : fin n → V} :
theorem linear_independent_fin_snoc {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {x : V} {n : } {v : fin n → V} :
theorem linear_independent.fin_cons {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {x : V} {n : } {v : fin n → V} (hv : linear_independent K v) (hx : x submodule.span K (set.range v)) :

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

theorem linear_independent_fin_succ {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {n : } {v : fin (n + 1) → V} :
theorem linear_independent_fin_succ' {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {n : } {v : fin (n + 1) → V} :
theorem linear_independent_fin2 {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {f : fin 2 → V} :
linear_independent K f f 1 0 ∀ (a : K), a f 1 f 0
theorem exists_linear_independent {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s t : set V} (hs : linear_independent K (λ (x : s), x)) (hst : s t) :
∃ (b : set V) (H : b t), s b t (submodule.span K b) linear_independent K (λ (x : b), x)
def linear_independent.extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s t : set V} (hs : linear_independent K (λ (x : s), x)) (hst : s t) :
set V

linear_independent.extend adds vectors to a linear independent set s ⊆ t until it spans all elements of t.

Equations
theorem linear_independent.extend_subset {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s t : set V} (hs : linear_independent K (λ (x : s), x)) (hst : s t) :
hs.extend hst t
theorem linear_independent.subset_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s t : set V} (hs : linear_independent K (λ (x : s), x)) (hst : s t) :
s hs.extend hst
theorem linear_independent.subset_span_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s t : set V} (hs : linear_independent K (λ (x : s), x)) (hst : s t) :
theorem linear_independent.linear_independent_extend {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s t : set V} (hs : linear_independent K (λ (x : s), x)) (hst : s t) :
theorem exists_of_linear_independent_of_finite_span {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s : set V} {t : finset V} (hs : linear_independent K (λ (x : s), x)) (hst : s (submodule.span K t)) :
∃ (t' : finset V), t' s t s t' t'.card = t.card
theorem exists_finite_card_le_of_finite_of_linear_independent_of_span {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [module K V] {s t : set V} (ht : t.finite) (hs : linear_independent K (λ (x : s), x)) (hst : s (submodule.span K t)) :