Linear independence #
This file collects consequences of linear (in)dependence and includes specialized tests for specific families of vectors, requiring more theory to state.
Main statements #
We prove several specialized tests for linear independence of families of vectors and of sets of vectors.
linearIndependent_option,linearIndependent_finCons,linearIndependent_finSucc,linearIndependent_finSnoc: type-specific tests for linear independence of families of vector fields;linearIndependent_insert,linearIndependent_pair: 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.
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
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
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)
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)
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)
theorem
iSupIndep_range_lsingle
(ι : Type u')
(R : Type u_2)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
iSupIndep fun (i : ι) => (Finsupp.lsingle i).range
theorem
LinearMap.iSupIndep_map
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M']
[Module R M]
[Module R M']
(f : M →ₗ[R] M')
(inj : Function.Injective ⇑f)
{m : ι → Submodule R M}
(ind : iSupIndep m)
:
iSupIndep fun (i : ι) => Submodule.map f (m i)
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)
:
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
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.
theorem
Submodule.codisjoint_span_image_of_codisjoint
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(hv : span R (Set.range v) = ⊤)
{s t : Set ι}
(hst : Codisjoint s t)
:
Codisjoint (span R (v '' s)) (span R (v '' t))
theorem
LinearIndependent.isCompl_span_image
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(h₁ : LinearIndependent R v)
(h₂ : Submodule.span R (Set.range v) = ⊤)
{s t : Set ι}
(hst : IsCompl s t)
:
IsCompl (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
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.lsum R (fun (x : ι) => R) ℕ) fun (i : ι) => LinearMap.id.smulRight (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
LinearIndependent.pair_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
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}
:
@[simp]
theorem
LinearIndependent.pair_neg_left_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
@[simp]
theorem
LinearIndependent.pair_neg_right_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
theorem
LinearIndependent.pair_smul_smul_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{u v : R}
(hu : IsUnit u)
(hv : IsUnit v)
:
theorem
LinearIndependent.pair_smul_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[IsDomain S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[Module.IsTorsionFree S R]
{u : S}
(hu : u ≠ 0)
:
@[simp]
theorem
LinearIndependent.pair_add_smul_add_smul_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[IsDomain S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[Module.IsTorsionFree S R]
(a b c d : S)
[Nontrivial R]
:
@[simp]
theorem
LinearIndependent.pair_add_smul_right_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[IsDomain S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[Module.IsTorsionFree S R]
(c : S)
:
@[simp]
theorem
LinearIndependent.pair_add_smul_left_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[IsDomain S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[Module.IsTorsionFree S R]
(b : S)
:
@[simp]
theorem
LinearIndependent.pair_add_right_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
@[simp]
theorem
LinearIndependent.pair_add_left_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
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)
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
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)
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]
:
theorem
LinearMap.injective_of_linearIndependent
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{N : Type u_6}
[AddCommGroup N]
[Module R N]
{f : M →ₗ[R] N}
{ι : Type u_7}
{v : ι → M}
(hv : Submodule.span R (Set.range v) = ⊤)
(hli : LinearIndependent R (⇑f ∘ v))
:
theorem
LinearMap.bijective_of_linearIndependent_of_span_eq_top
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{N : Type u_6}
[AddCommGroup N]
[Module R N]
{f : M →ₗ[R] N}
{ι : Type u_7}
{v : ι → M}
(hv : Submodule.span R (Set.range v) = ⊤)
(hli : LinearIndependent R (⇑f ∘ v))
(hsp : Submodule.span R (Set.range (⇑f ∘ v)) = ⊤)
:
theorem
LinearIndepOn.insert'
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
{i : ι}
(hs : LinearIndepOn R v s)
(hx : ∀ (r : R), r • v i ∈ Submodule.span R (v '' s) → r = 0)
:
LinearIndepOn R v (insert i s)
Version of LinearIndepOn.insert that works when the scalars are not a field.
theorem
LinearIndepOn.id_insert'
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
{x : M}
(hs : LinearIndepOn R id s)
(hx : ∀ (r : R), r • x ∈ Submodule.span R s → r = 0)
:
LinearIndepOn R id (insert x s)
Version of LinearIndepOn.id_insert that works when the scalars are not a field.
theorem
LinearIndependent.of_pairwise_dual_eq_zero_one
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(v : ι → M)
(f : ι → Module.Dual R M)
(h1 : Pairwise fun (i j : ι) => (f i) (v j) = 0)
(h2 : ∀ (i : ι), (f i) (v i) = 1)
:
If v : ι → M is a family of vectors and there exists a family of linear forms
f : ι → Dual R M such that f i (v j) is 1 for i = j and 0 for i ≠ j, then
v is linearly independent.
theorem
LinearIndependent.update
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[DecidableEq ι]
[CommRing R]
[AddCommGroup M]
[Module R M]
{f : ι → M}
(hf : LinearIndependent R f)
(i : ι)
(m : M)
(hg : ∃ r ∈ nonZeroDivisors R, ∃ (l : ι →₀ R), l i ∈ nonZeroDivisors R ∧ r • m = (Finsupp.linearCombination R f) l)
:
LinearIndependent R (Function.update f i m)
A linearly independent family of vectors f remains linearly independent when we substitute one
of the terms with a vector m provided there exists a non-zero divisor r, such that r • m
belongs to the span of f with non-zero-divisor coefficients.
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
LinearIndepOn.insert
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s : Set ι}
{x : ι}
(hs : LinearIndepOn K v s)
(hx : v x ∉ Submodule.span K (v '' s))
:
LinearIndepOn K v (insert x s)
theorem
LinearIndepOn.id_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)
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)
:
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)
:
theorem
linearIndepOn_insert_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
:
theorem
linearIndepOn_id_insert_iff
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{a : V}
{s : Set V}
:
theorem
LinearIndepOn.mem_span_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(h : LinearIndepOn K f s)
:
theorem
LinearIndepOn.notMem_span_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(h : LinearIndepOn K f s)
:
A shortcut to a convenient form for the negation in LinearIndepOn.mem_span_iff.
theorem
LinearIndepOn.mem_span_iff_id
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{a : V}
(h : LinearIndepOn K id s)
:
theorem
LinearIndepOn.notMem_span_iff_id
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{a : V}
(h : LinearIndepOn K id s)
:
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}
theorem
linearIndepOn_pair_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{i j : ι}
(v : ι → V)
(hij : i ≠ j)
(hi : v i ≠ 0)
:
LinearIndepOn.pair_iff is a version that works over arbitrary rings.
theorem
LinearIndependent.pair_iff'
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x y : V}
(hx : x ≠ 0)
:
Also see LinearIndependent.pair_iff for the version over arbitrary rings.
theorem
linearIndependent_finCons
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
:
@[deprecated linearIndependent_finCons (since := "2026-04-07")]
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}
:
Alias of linearIndependent_finCons.
theorem
linearIndependent_finSnoc
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
:
@[deprecated linearIndependent_finSnoc (since := "2026-04-07")]
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}
:
Alias of linearIndependent_finSnoc.
theorem
LinearIndependent.finCons
{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.finCons' for an uglier version that works if you
only have a module over a semiring.
@[deprecated LinearIndependent.finCons (since := "2026-04-07")]
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)
Alias of LinearIndependent.finCons.
See LinearIndependent.finCons' for an uglier version that works if you
only have a module over a semiring.
theorem
LinearIndependent.finSnoc
{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.snoc v x)
See LinearIndependent.finSnoc' for an uglier version that works if you
only have a module over a semiring, and LinearIndependent.finSnoc_of_not_mem_span_over for a
version over a subring of a division ring.
theorem
LinearIndependent.finSnoc_of_not_mem_span_over
{R : Type u_6}
{K : Type u_7}
{M : Type u_8}
[CommRing R]
[DivisionRing K]
[AddCommGroup M]
[Algebra R K]
[Module K M]
[Module R M]
[IsScalarTower R K M]
[FaithfulSMul R K]
{n : ℕ}
{v : Fin n → M}
(hv : LinearIndependent R v)
{x : M}
(hx : x ∉ Submodule.span K (Set.range v))
:
LinearIndependent R (Fin.snoc v x)
If v is R-linearly independent and x is not in the K-span of range v (where K is a
division ring extending R and acting on the same module), then Fin.snoc v x is R-linearly
independent.
This is useful when proving ℤ-linear independence using the fact that an element is outside the
ℝ-span, which arises naturally in lattice theory and geometry of numbers.
theorem
linearIndependent_finSucc
{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))
@[deprecated linearIndependent_finSucc (since := "2026-04-07")]
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))
Alias of linearIndependent_finSucc.
theorem
linearIndependent_finSucc'
{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))
@[deprecated linearIndependent_finSucc' (since := "2026-04-07")]
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))
Alias of linearIndependent_finSucc'.
def
equiv_linearIndependent
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(n : ℕ)
:
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.
Instances For
theorem
linearIndependent_fin2
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{f : Fin 2 → V}
:
theorem
exists_linearIndepOn_extension
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s t : Set ι}
(hs : LinearIndepOn K v s)
(hst : s ⊆ t)
:
∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ ↑(Submodule.span K (v '' b)) ∧ LinearIndepOn K v b
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
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
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s t : Set ι}
(hs : LinearIndepOn K v s)
(hst : s ⊆ t)
:
Set ι
LinearIndepOn.extend adds vectors to a linear independent set s ⊆ t until it spans
all elements of t.
Equations
- hs.extend hst = Classical.choose ⋯
Instances For
theorem
LinearIndepOn.extend_subset
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s t : Set ι}
(hs : LinearIndepOn K v s)
(hst : s ⊆ t)
:
hs.extend hst ⊆ t
theorem
LinearIndepOn.subset_extend
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s t : Set ι}
(hs : LinearIndepOn K v s)
(hst : s ⊆ t)
:
s ⊆ hs.extend hst
theorem
LinearIndepOn.image_subset_span_image_extend
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s t : Set ι}
(hs : LinearIndepOn K v s)
(hst : s ⊆ t)
:
v '' t ⊆ ↑(Submodule.span K (v '' hs.extend hst))
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))
theorem
LinearIndepOn.span_image_extend_eq_span_image
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s t : Set ι}
(hs : LinearIndepOn K v s)
(hst : s ⊆ t)
:
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)
:
theorem
LinearIndepOn.linearIndepOn_extend
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{s t : Set ι}
(hs : LinearIndepOn K v s)
(hst : s ⊆ t)
:
LinearIndepOn K v (hs.extend hst)
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))
:
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))
: