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 vstates that the elements of the familyvare linearly independent.LinearIndependent.repr hv xreturns the linear combination representingx : span R (range v)on the linearly independent vectorsv, givenhv : LinearIndependent R v(using classical choice).LinearIndependent.repr hvis 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 functionf : ι → Rhas finite support, so we can reformulate the statement using∑ i : ι, f i • v iinstead of a sum over an auxiliarys : Finset ι;linearIndependent_empty_type: a family indexed by an empty type is linearly independent;linearIndependent_unique_iff: ifιis a singleton, thenLinearIndependent K vis equivalent tov 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 use sets, use the family (fun x ↦ x : s → M) given a set s : Set M. The lemmas
LinearIndependent.to_subtype_range and LinearIndependent.of_subtype_range 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]
:
LinearIndependent R v states the family of vectors v is linearly independent over R.
Equations
Instances For
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.
Instances For
theorem
linearIndependent_iff_injective_linearCombination
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
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
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
linearIndependent_empty_type
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsEmpty ι]
:
theorem
linearIndependent_empty
(R : Type u_2)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
LinearIndependent R fun (x : ↑∅) => ↑x
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)
:
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.
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]
:
theorem
linearIndependent_iff''
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
:
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
LinearIndependent.eq_zero_of_pair
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
(h : LinearIndependent R ![x, y])
{s t : R}
(h' : s • x + t • y = 0)
:
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_iff_finset_linearIndependent
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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
LinearIndependent.coe_range
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(i : LinearIndependent R v)
:
LinearIndependent R Subtype.val
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
Submodule.range_ker_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'}
(hv : LinearIndependent R (⇑f ∘ v))
:
Disjoint (Submodule.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
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 : ZeroHom 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
LinearIndependent.of_comp
{ι : 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')
(hfv : LinearIndependent 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
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 : LinearMap.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_of_subsingleton
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Subsingleton R]
:
theorem
linearIndependent_equiv
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup M]
[Module R M]
(e : ι ≃ ι')
{f : ι' → M}
{g : ι → M}
(h : f ∘ ⇑e = g)
:
LinearIndependent R g ↔ LinearIndependent R f
theorem
linearIndependent_subtype_range
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : Function.Injective f)
:
LinearIndependent R Subtype.val ↔ LinearIndependent R f
theorem
LinearIndependent.of_subtype_range
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : Function.Injective f)
:
LinearIndependent R Subtype.val → LinearIndependent R f
Alias of the forward direction of linearIndependent_subtype_range.
theorem
linearIndependent_image
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{s : Set ι}
{f : ι → M}
(hf : Set.InjOn f s)
:
(LinearIndependent R fun (x : ↑s) => f ↑x) ↔ LinearIndependent R fun (x : ↑(f '' s)) => ↑x
theorem
linearIndependent_span
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hs : LinearIndependent R v)
:
LinearIndependent R fun (i : ι) => ⟨v i, ⋯⟩
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.
theorem
linearIndependent_finset_map_embedding_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup 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.
The following lemmas use the subtype defined by a set in M as the index set ι.
theorem
linearIndependent_comp_subtype
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
theorem
linearDependent_comp_subtype'
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = 0 ∧ f ≠ 0
theorem
linearDependent_comp_subtype
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∃ f ∈ Finsupp.supported R R s, ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0
A version of linearDependent_comp_subtype' with Finsupp.linearCombination unfolded.
theorem
linearIndependent_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R id) l = 0 → l = 0
theorem
linearIndependent_comp_subtype_disjoint
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
theorem
linearIndependent_subtype_disjoint
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R id))
theorem
linearIndependent_iff_linearCombinationOn
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ LinearMap.ker (Finsupp.linearCombinationOn M M R id s) = ⊥
@[deprecated linearIndependent_iff_linearCombinationOn]
theorem
linearIndependent_iff_totalOn
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ LinearMap.ker (Finsupp.linearCombinationOn M M R id s) = ⊥
theorem
LinearIndependent.restrict_of_comp_subtype
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
(hs : LinearIndependent (ι := ↑s) R (v ∘ Subtype.val))
:
LinearIndependent (ι := ↑s) R (s.restrict v)
theorem
LinearIndependent.mono
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{t s : Set M}
(h : t ⊆ s)
:
(LinearIndependent R fun (x : ↑s) => ↑x) → LinearIndependent R fun (x : ↑t) => ↑x
theorem
linearIndependent_of_finite
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : Set M)
(H : ∀ t ⊆ s, t.Finite → LinearIndependent R fun (x : ↑t) => ↑x)
:
LinearIndependent R fun (x : ↑s) => ↑x
theorem
linearIndependent_iUnion_of_directed
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{η : Type u_6}
{s : η → Set M}
(hs : Directed (fun (x1 x2 : Set M) => x1 ⊆ x2) s)
(h : ∀ (i : η), LinearIndependent R fun (x : ↑(s i)) => ↑x)
:
LinearIndependent R fun (x : ↑(⋃ (i : η), s i)) => ↑x
theorem
linearIndependent_sUnion_of_directed
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set (Set M)}
(hs : DirectedOn (fun (x1 x2 : Set M) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndependent R Subtype.val)
:
LinearIndependent R fun (x : ↑(⋃₀ s)) => ↑x
theorem
linearIndependent_biUnion_of_directed
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{η : Type u_6}
{s : Set η}
{t : η → Set M}
(hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set M) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndependent R fun (x : ↑(t a)) => ↑x)
:
LinearIndependent R fun (x : ↑(⋃ a ∈ s, t a)) => ↑x
@[deprecated linearIndependent_iff_injective_linearCombination]
theorem
linearIndependent_iff_injective_total
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
@[deprecated LinearIndependent.injective_linearCombination]
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.injective
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(hv : LinearIndependent R v)
:
theorem
LinearIndependent.to_subtype_range
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : LinearIndependent R f)
:
LinearIndependent R Subtype.val
theorem
LinearIndependent.to_subtype_range'
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : LinearIndependent R f)
{t : Set M}
(ht : Set.range f = t)
:
LinearIndependent R Subtype.val
theorem
LinearIndependent.image_of_comp
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{ι' : Type u_7}
(s : Set ι)
(f : ι → ι')
(g : ι' → M)
(hs : LinearIndependent R fun (x : ↑s) => g (f ↑x))
:
LinearIndependent R fun (x : ↑(f '' s)) => g ↑x
theorem
LinearIndependent.image
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{s : Set ι}
{f : ι → M}
(hs : LinearIndependent R fun (x : ↑s) => f ↑x)
:
LinearIndependent R fun (x : ↑(f '' s)) => ↑x
theorem
LinearIndependent.group_smul
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup 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)
theorem
LinearIndependent.units_smul
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{v : ι → M}
(hv : LinearIndependent R v)
(w : ι → Rˣ)
:
LinearIndependent R (w • v)
theorem
LinearIndependent.eq_zero_of_pair'
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
(h : LinearIndependent R ![x, y])
{s t : R}
(h' : s • x = t • y)
:
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)
:
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.
def
LinearIndependent.Maximal
{ι : Type w}
{R : Type u}
[Ring R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{v : ι → M}
(_i : LinearIndependent R v)
:
A linearly independent family is maximal if there is no strictly larger linearly independent family.
Equations
Instances For
theorem
LinearIndependent.maximal_iff
{ι : Type w}
{R : Type u}
[Ring R]
[Nontrivial R]
{M : Type v}
[AddCommGroup 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
LinearIndependent.eq_of_smul_apply_eq_smul_apply
{ι : Type u'}
{R : Type u_2}
[Ring R]
{M : Type u_6}
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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]
theorem
LinearIndependent.total_ne_of_not_mem_support
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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.
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
LinearIndependent.union
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s t : Set M}
(hs : LinearIndependent R fun (x : ↑s) => ↑x)
(ht : LinearIndependent R fun (x : ↑t) => ↑x)
(hst : Disjoint (Submodule.span R s) (Submodule.span R t))
:
LinearIndependent R fun (x : ↑(s ∪ t)) => ↑x
theorem
linearIndependent_iUnion_finite_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → Set M}
(hl : ∀ (i : ι), LinearIndependent R fun (x : ↑(f i)) => ↑x)
(hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i)))
:
LinearIndependent R fun (x : ↑(⋃ (i : ι), f i)) => ↑x
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
def
LinearIndependent.linearCombinationEquiv
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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) ⋯) ⋯
Instances For
@[simp]
theorem
LinearIndependent.linearCombinationEquiv_symm_apply
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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]
def
LinearIndependent.totalEquiv
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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.
Instances For
@[simp]
theorem
LinearIndependent.linearCombinationEquiv_apply_coe
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
(l : ι →₀ R)
:
↑(hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
@[deprecated LinearIndependent.linearCombinationEquiv_apply_coe]
theorem
LinearIndependent.totalEquiv_apply_coe
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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
Instances For
@[simp]
theorem
LinearIndependent.linearCombination_repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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]
theorem
LinearIndependent.total_repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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]
theorem
LinearIndependent.total_comp_repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
Finsupp.linearCombination R v ∘ₗ hv.repr = (Submodule.span R (Set.range v)).subtype
theorem
LinearIndependent.repr_ker
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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}
[Ring R]
[AddCommGroup 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_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
LinearIndependent.iSupIndep_span_singleton
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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]
theorem
LinearIndependent.independent_span_singleton
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup 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
exists_maximal_independent'
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : ι → M)
:
∃ (I : Set ι),
(LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun (x : ↑J) => s ↑x) → I = J
theorem
exists_maximal_independent
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : ι → M)
:
∃ (I : Set ι),
(LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ a • s i ∈ Submodule.span R (s '' I)
theorem
surjective_of_linearIndependent_of_span
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(hv : LinearIndependent R v)
(f : ι' ↪ ι)
(hss : Set.range v ⊆ ↑(Submodule.span R (Set.range (v ∘ ⇑f))))
:
theorem
eq_of_linearIndependent_of_span_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
{s t : Set M}
(hs : LinearIndependent R fun (x : ↑s) => ↑x)
(h : t ⊆ s)
(hst : s ⊆ ↑(Submodule.span R t))
:
s = t
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 : LinearIndependent R fun (x : ↑s) => ↑x)
(hf_inj : Disjoint (Submodule.span R s) (LinearMap.ker f))
:
LinearIndependent R fun (x : ↑(⇑f '' s)) => ↑x
theorem
LinearIndependent.inl_union_inr
{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}
{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
linearIndependent_inl_union_inr'
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
[Ring R]
[AddCommGroup M]
[AddCommGroup 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_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
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
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
le_of_span_le_span
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
{s t u : Set M}
(hl : LinearIndependent R Subtype.val)
(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}
[Ring R]
[AddCommGroup 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_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
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)
:
LinearIndependent R fun (x_1 : ↑{x}) => ↑x_1
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
LinearIndependent.insert
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
(hs : LinearIndependent K fun (b : ↑s) => ↑b)
(hx : x ∉ Submodule.span K s)
:
LinearIndependent K fun (b : ↑(insert x s)) => ↑b
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
linearIndependent_insert'
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_6}
{s : Set ι}
{a : ι}
{f : ι → V}
(has : a ∉ s)
:
(LinearIndependent K fun (x : ↑(insert a s)) => f ↑x) ↔ (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ Submodule.span K (f '' s)
theorem
linearIndependent_insert
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
(hxs : x ∉ s)
:
(LinearIndependent K fun (b : ↑(insert x s)) => ↑b) ↔ (LinearIndependent K fun (b : ↑s) => ↑b) ∧ x ∉ Submodule.span K s
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)
:
LinearIndependent K Subtype.val
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.
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_linearIndependent_extension
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndependent K Subtype.val)
(hst : s ⊆ t)
:
∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndependent K Subtype.val
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
noncomputable def
LinearIndependent.extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
Set V
LinearIndependent.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
LinearIndependent.extend_subset
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
hs.extend hst ⊆ t
theorem
LinearIndependent.subset_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
s ⊆ hs.extend hst
theorem
LinearIndependent.subset_span_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
t ⊆ ↑(Submodule.span K (hs.extend hst))
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 : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
Submodule.span K (hs.extend hst) = Submodule.span K t
theorem
LinearIndependent.linearIndependent_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
LinearIndependent K Subtype.val
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 : LinearIndependent K fun (x : ↑s) => ↑x)
(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 : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ ↑(Submodule.span K t))
:
∃ (h : s.Finite), h.toFinset.card ≤ ht.toFinset.card