LinearIndependent.comp
theorem LinearIndependent.comp :
∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : Module R M],
LinearIndependent R v → ∀ (f : ι' → ι), Function.Injective f → LinearIndependent R (v ∘ f)
This theorem states that if you have a family of vectors `v` that is linearly independent over a semiring `R`, and if you have an injective function `f` that maps from one type `ι'` to another type `ι`, then the subfamily of vectors obtained by composing `v` and `f` (i.e., `v ∘ f`) is also linearly independent over `R`. In other words, a subfamily of a linearly independent family, obtained through an injective map, remains linearly independent. This theorem holds for semirings `R` and modules `M` that are additively commutative monoids.
More concisely: If `{v\_i : V}` is a linearly independent family of vectors over a commutative additive monoid `M` as a semiring, and `f : ι' -> ι` is an injective function, then `{v\_i ∘ f : V}` is a linearly independent family of vectors over `M`.
|
linearIndependent_unique
theorem linearIndependent_unique :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : NoZeroSMulDivisors R M] (v : ι → M) [inst_5 : Unique ι],
v default ≠ 0 → LinearIndependent R v
The theorem `linearIndependent_unique` states that for any types `ι`, `R`, and `M`; given a ring `R` that is nontrivial, an additive commutative group `M`, a module over `R` and `M`, and an assumption that there are no zero scalar multipliers and dividers between `R` and `M`; if `v` is a function from `ι` to `M` where `ι` is unique, and the default of `v` is not zero, then the family of vectors `v` is linearly independent over `R`. In other words, for a unique index type, if the mapped vector is non-zero, then the vector is linearly independent.
More concisely: Given a nontrivial ring `R`, an additive commutative group `M` with no zero scalar multipliers or dividers, and a function `v : ι -> M` from a unique index type `ι` with non-zero default value, then the family `{v i : M | i ∈ ι}` is linearly independent over `R`.
|
linearIndependent_bounded_of_finset_linearIndependent_bounded
theorem linearIndependent_bounded_of_finset_linearIndependent_bounded :
∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
(∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n) →
∀ (s : Set M), LinearIndependent (ι := { x // x ∈ s }) R Subtype.val → Cardinal.mk ↑s ≤ ↑n
This theorem states that if every finite set of linearly independent vectors over a semiring `R` in a module `M` has cardinality at most `n`, then the same is true for arbitrary (possibly infinite) sets of linearly independent vectors.
In other words, if for every finite subset `s` of `M`, if `s` is a set of linearly independent vectors, then the number of elements in `s` is less than or equal to `n`. Under these conditions, for any set `t` in `M`, if `t` is also a set of linearly independent vectors, then the cardinality of `t` is less than or equal to `n`.
The `LinearIndependent R fun i => ↑i` part denotes that the vectors in the set are linearly independent over `R`, and the `s.card ≤ n` and `Cardinal.mk ↑s ≤ ↑n` parts specify that the size of the vector set is less than or equal to `n`.
More concisely: If every finite set of linearly independent vectors in a module over a semiring has cardinality at most n, then every infinite set of linearly independent vectors also has cardinality at most n.
|
LinearIndependent.of_comp
theorem LinearIndependent.of_comp :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M']
(f : M →ₗ[R] M'), LinearIndependent R (⇑f ∘ v) → LinearIndependent R v
The theorem `LinearIndependent.of_comp` states that for any semiring `R` and additive commutative monoids `M` and `M'` that are also `R`-modules, given a linear map `f` from `M` to `M'` and a family of vectors `v`, if the image of the family of vectors under the linear map is linearly independent over `R`, then the original family of vectors is also linearly independent over `R`.
More concisely: If `f : M → M'` is a linear map between additive commutative `R`-modules `M` and `M'`, and the image of a family of vectors in `M` under `f` is linearly independent over `R`, then the original family of vectors is also linearly independent over `R`.
|
LinearIndependent.injective
theorem LinearIndependent.injective :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : Nontrivial R], LinearIndependent R v → Function.Injective v
The theorem `LinearIndependent.injective` states that for any type 'ι', ring 'R', and additive commutative group 'M', if the function 'v : ι → M' is linearly independent over 'R', then 'v' is injective. Here, a function is said to be injective if for any two elements 'a₁' and 'a₂' from the domain, if 'v(a₁) = v(a₂)' then 'a₁ = a₂'. Similarly, a family of vectors is said to be linearly independent if no vector can be represented as a linear combination of the others. The theorem assumes that 'R' is nontrivial, meaning it has at least two distinct elements.
More concisely: If 'v' is a function from a type 'ι' to an additive commutative group 'M' over a nontrivial ring 'R', and 'v' is linearly independent over 'R', then 'v' is injective.
|
Submodule.range_ker_disjoint
theorem Submodule.range_ker_disjoint :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M']
{f : M →ₗ[R] M'}, LinearIndependent R (⇑f ∘ v) → Disjoint (Submodule.span R (Set.range v)) (LinearMap.ker f)
The theorem `Submodule.range_ker_disjoint` states that for any injective family of vectors `v`, if `f ∘ v` is linearly independent over a semiring `R`, then the smallest submodule of the module `M` that contains the set `v` (i.e., the span of `v`) is disjoint from the kernel of `f`. Here, `Disjoint` means that the intersection (infimum) of the two submodules is the bottom element. In other words, there are no common elements in the span of `v` and the kernel of `f`, except for the zero vector. The modules `M` and `M'` have addition operation that is commutative and `M` and `M'` are both `R`-modules. The function `f` is a linear map from `M` to `M'`.
More concisely: If `v` is an injective family of vectors in an `R`-module `M` such that `f ∘ v` is linearly independent over `R`, then the span of `v` and the kernel of `f` have an empty intersection in `M`, except for the zero vector.
|
linearIndependent_iUnion_of_directed
theorem linearIndependent_iUnion_of_directed :
∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {η : Type u_8}
{s : η → Set M},
Directed (fun x x_1 => x ⊆ x_1) s →
(∀ (i : η), LinearIndependent R fun (x : ↑(s i)) => ↑x) → LinearIndependent R fun (x : ↑(⋃ i, s i)) => ↑x
This theorem states that for any semiring `R`, additive commutative monoid `M`, and any module over `R` and `M`, given a directed family of sets of elements of `M`, if each set in the family is linearly independent over `R`, then the union of all these sets is also linearly independent over `R`. Here, a family of sets is directed if, for any two sets in the family, there exists another set in the family that contains both of the initial sets. Linear independence of a set means that no vector in the set can be written as a linear combination of the other vectors in the set.
More concisely: If `{A_i}` is a directed family of linearly independent sets in an `R`-module `M`, then their union is also linearly independent in `M` over `R`.
|
linearIndependent_equiv
theorem linearIndependent_equiv :
∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (e : ι ≃ ι') {f : ι' → M}, LinearIndependent R (f ∘ ⇑e) ↔ LinearIndependent R f
The theorem `linearIndependent_equiv` asserts that for any two types `ι` and `ι'`, a type `R` that is a semiring, a type `M` that is an additive commutative monoid and a module over `R`, and an equivalence `e` between `ι` and `ι'`, the family of vectors `f` is linearly independent over `R` if and only if the family of vectors obtained by applying `f` after the map induced by `e` is also linearly independent over `R`. This means that the linear independence of a family of vectors is preserved under the re-indexing of the basis vectors.
More concisely: Given types `ι` and `ι'`, a semiring `R`, an additive commutative monoid and `R`-module `M`, and an equivalence `e` between `ι` and `ι'`, the family `{x_i : M | i ∈ ι}` is linearly independent over `R` if and only if the family `{x_i' : M | i' = e(i) for i ∈ ι}` is linearly independent over `R`.
|
LinearMap.linearIndependent_iff
theorem LinearMap.linearIndependent_iff :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M']
(f : M →ₗ[R] M'), LinearMap.ker f = ⊥ → (LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v)
The theorem `LinearMap.linearIndependent_iff` states that for a given injective linear map `f`, a family of vectors `f ∘ v` is linearly independent if and only if the original family of vectors `v` is linearly independent. This theorem applies in the context where `R` is a semiring, `M` and `M'` are additive commutative monoids with a module structure over `R`, and `v` is a family of vectors in `M`. The injectivity of `f` is expressed by the condition that the kernel of `f` is the trivial submodule.
More concisely: A family of vectors in an additive commutative monoid endowed with an R-module structure is linearly independent if and only if the image of that family under an injective linear map from another such monoid is linearly independent.
|
LinearIndependent.restrict_scalars
theorem LinearIndependent.restrict_scalars :
∀ {ι : Type u'} {R : Type u_2} {K : Type u_3} {M : Type u_4} {v : ι → M} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : Semiring K] [inst_4 : SMulWithZero R K]
[inst_5 : Module K M] [inst_6 : IsScalarTower R K M],
(Function.Injective fun r => r • 1) → LinearIndependent K v → LinearIndependent R v
This theorem, `LinearIndependent.restrict_scalars`, states that if we have a set of vectors `v` that is linearly independent over a semiring `K` in a module `M`, these vectors remain linearly independent when we look at them over a subring `R` of `K`. The function that maps each element of `R` to its scalar multiplication with 1 must be injective for this to hold. This theorem operates under minimal assumptions about how `R`, `K`, and `M` interact. There is a different version of this theorem, `LinearIndependent.restrict_scalars_algebras`, for the case where `K` is an `R`-algebra.
More concisely: If `v` is a linearly independent set of vectors in the module `M` over the semiring `K`, and the inclusion map from the subring `R` to `K` is an injection, then `v` is also linearly independent in `M` over `R`.
|
linearIndependent_singleton
theorem linearIndependent_singleton :
∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : NoZeroSMulDivisors R M] {x : M},
x ≠ 0 → LinearIndependent R fun (x_1 : ↑{x}) => ↑x_1
This theorem, `linearIndependent_singleton`, states that for any ring `R`, given a nontrivial element `x` from the additive commutative group `M` (which is also a module over `R`) such that `R` and `M` have no zero scalar multiplication-divisors, if `x` is not equal to zero, then the function mapping each element of the singleton set `{x}` to `x` itself results in a linearly independent set of vectors over `R`. In other words, a non-zero element in a module forms a linearly independent set.
More concisely: If `R` is a ring with no zero divisors, and `M` is an additive commutative group over `R` with no zero scalar multiplication-divisors, then a non-zero element `x` in `M` forms a linearly independent set.
|
LinearIndependent.map
theorem LinearIndependent.map :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'],
LinearIndependent R v →
∀ {f : M →ₗ[R] M'},
Disjoint (Submodule.span R (Set.range v)) (LinearMap.ker f) → LinearIndependent R (⇑f ∘ v)
The theorem is stating that if we have a linearly independent family of vectors 'v' and the kernel of a linear map 'f' is disjoint with the submodule spanned by the vectors of 'v', then the composition of 'f' and 'v' is also a linearly independent family of vectors. It does this within the context of a semiring 'R' and two additively commutative monoids 'M' and 'M''. This means that no vector in the span of 'v' is mapped to zero by 'f', unless it is the zero vector itself. The theorem essentially preserves the property of linear independence through the linear map if the aforementioned conditions are met.
More concisely: If 'v' is a linearly independent family of vectors in an additively commutative monoid 'M' over a semiring 'R', and the kernel of a linear map 'f' from 'M' to another additively commutative monoid 'N' does not intersect the submodule spanned by 'v', then the image of 'v' under 'f' is also a linearly independent family of vectors in 'N'.
|
LinearIndependent.ne_zero
theorem LinearIndependent.ne_zero :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Nontrivial R] (i : ι), LinearIndependent R v → v i ≠ 0
The theorem `LinearIndependent.ne_zero` states that for any type `ι`, semiring `R`, additively commutative monoid `M`, function `v` mapping from `ι` to `M`, module structure on `R` and `M`, and nontrivial structure on `R`, if `v` is a family of vectors that is defined to be linearly independent over `R`, then each individual vector in the family (represented by `v i`) is not equal to zero. In other words, no vector in a linearly independent family can be the zero vector.
More concisely: Given a type ι, a semiring R, an additively commutative monoid M with a module structure over R, a nontrivial R-module M, and a linearly independent family {vi : M | i ∈ ι} over R, then vi ≠ 0 for all i ∈ ι.
|
linearIndependent_iff
theorem linearIndependent_iff :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M], LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.total ι M R v) l = 0 → l = 0
The theorem `linearIndependent_iff` states that for any types ι, R, and M, and any function `v` from ι to M, given a semiring structure on R, an additive commutative monoid structure on M, and a module structure over R on M, the function `v` is linearly independent over R if and only if for every linear combination `l` (represented as a function from ι to R), if the total of `l` under `v` equals zero, then `l` must be the zero function. In other words, no non-trivial linear combination of the vectors given by `v` can sum to the zero vector, which is the definition of linear independence in linear algebra.
More concisely: A function from a type to a module is linearly independent over a semiring if and only if no non-trivial linear combination of its images sums to the zero vector.
|
linearIndependent_iff_finset_linearIndependent
theorem linearIndependent_iff_finset_linearIndependent :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M], LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
This theorem states that a family of vectors is linearly independent over a semiring R if and only if every finite subfamily of this family is also linearly independent over R. In other words, for any type ι, a semiring R, an additively commutative monoid M, and a function v mapping ι to M, the function v is linearly independent (in the sense of the `LinearIndependent` definition) if and only if for every finite subset s of ι, the function obtained by composing v and the value function of the subtype of s (i.e., `v ∘ Subtype.val`) is also linearly independent. Here, `Subtype.val` extracts the underlying element from a subtype where the property p holds.
More concisely: A family of vectors is linearly independent over a semiring if and only if every finite subfamily is also linearly independent.
|
LinearIndependent.eq_of_smul_apply_eq_smul_apply
theorem LinearIndependent.eq_of_smul_apply_eq_smul_apply :
∀ {ι : Type u'} {R : Type u_2} [inst : Ring R] {M : Type u_8} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{v : ι → M}, LinearIndependent R v → ∀ (c d : R) (i j : ι), c ≠ 0 → c • v i = d • v j → i = j
The theorem `LinearIndependent.eq_of_smul_apply_eq_smul_apply` states that for a family of vectors `v` which are linearly independent over a ring `R`, if the scalar multiples of any two vectors in the family are equal (i.e., `c • v i = d • v j`), and the scalar `c` is non-zero, then those two vectors must be the same vector (i.e., `i = j`). This holds regardless of the specific scalars `c` and `d` used for the multiplication. This theorem essentially establishes that linear independence implies injectivity, even when scaling the vectors.
More concisely: If `{vi : V}` is a linearly independent family in a vector space `V` over a ring `R`, and for some indices `i ≠ j` and scalars `c, d ∈ R`, we have `c • vi = d • vj` with `c ≠ 0`, then `vi = vj`.
|
LinearIndependent.mono
theorem LinearIndependent.mono :
∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {t s : Set M},
t ⊆ s → (LinearIndependent R fun (x : ↑s) => ↑x) → LinearIndependent R fun (x : ↑t) => ↑x
The theorem `LinearIndependent.mono` states that for any semiring `R`, any set `M` endowed with the structure of an additive commutative monoid and an `R`-module, and any two subsets `t` and `s` of `M`, if `t` is a subset of `s`, and if the family of vectors indexed by `s` is linearly independent over `R`, then the family of vectors indexed by `t` is also linearly independent over `R`. In other words, if a set of vectors is linearly independent, then any subset of that set is also linearly independent.
More concisely: If a subset of a linearly independent set in an `R`-module over a semiring `R` is included in the original set, then the smaller subset is also linearly independent.
|
linearIndependent_monoidHom
theorem linearIndependent_monoidHom :
∀ (G : Type u_8) [inst : Monoid G] (L : Type u_9) [inst_1 : CommRing L] [inst_2 : NoZeroDivisors L],
LinearIndependent L fun f => ⇑f
"Dedekind's Linear Independence of Characters" theorem states that for any monoid `G` and any commutative ring `L` that has no zero divisors, the set of all functions from `G` to `L` that are monoid homomorphisms (i.e., respect the operation of the monoid and map the identity element of the monoid to the identity element of the ring) is linearly independent over `L`. In other words, no non-trivial linear combination of these functions can result in the zero function.
More concisely: The set of monoid homomorphisms from a monoid to a commutative ring without zero divisors is linearly independent.
|
LinearIndependent.independent_span_singleton
theorem LinearIndependent.independent_span_singleton :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M], LinearIndependent R v → CompleteLattice.Independent fun i => Submodule.span R {v i}
This theorem states that for any type `ι`, a ring `R`, an additive commutative group `M`, and a function `v` from `ι` to `M`, if `v` is linearly independent over `R`, then for each `i` in `ι`, the span of the singleton set `{v i}` is a complete lattice independent set. In other words, the vector space spans of the individual vectors of a linearly independent set are mutually independent in the sense of lattice theory.
More concisely: For any type `ι`, ring `R`, additive commutative group `M`, and linearly independent function `v` from `ι` to `M`, the span of each singleton `{vi}` forms a complete lattice independent set in the lattice of subspaces of `M` over `R`.
|
LinearIndependent.to_subtype_range
theorem LinearIndependent.to_subtype_range :
∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_8}
{f : ι → M}, LinearIndependent R f → LinearIndependent (ι := { x // x ∈ Set.range f }) R Subtype.val
The theorem `LinearIndependent.to_subtype_range` states that for any ring `R`, any additive commutative group `M`, and any module structure on `M` over `R`, if a function `f` from a type `ι` to `M` is linearly independent over `R`, then the function `Subtype.val`, which returns the underlying elements of the set `{x // x ∈ range of f}`, is also linearly independent over `R`. In other words, restriction of a linearly independent set to the range of its defining function preserves linear independence.
More concisely: If `f` is a linearly independent function from type `ι` to the module `M` over ring `R`, then the image of `f` is a linearly independent subset of `M`.
|
LinearIndependent.map_of_injective_injective
theorem LinearIndependent.map_of_injective_injective :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {R' : Type u_8} {M' : Type u_9} [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M']
[inst_5 : Module R' M'],
LinearIndependent R v →
∀ (i : R' → R) (j : M →+ M'),
(∀ (r : R'), i r = 0 → r = 0) →
(∀ (m : M), j m = 0 → m = 0) →
(∀ (r : R') (m : M), j (i r • m) = r • j m) → LinearIndependent R' (⇑j ∘ v)
The theorem `LinearIndependent.map_of_injective_injective` states that given two modules `M / R` and `M' / R'`, if we have a map `i : R' → R` and a monoid map `j : M →+ M'` such that they map non-zero elements to non-zero elements, and are compatible with the scalar multiplications on `M` and `M'`, then if a family of vectors `v` is linearly independent in `M / R`, their images under `j` form a linearly independent family of vectors in `M' / R'`. This theorem also covers the special case where `R = R'` as `LinearIndependent.map'`.
More concisely: If `i : R' → R` is a ring homomorphism, `j : M →+ M'` is a module homomorphism between modules `M / R` and `M' / R'`, and `v : Finset M` is a linearly independent family in `M / R`, then `j (Map v)` is a linearly independent family in `M' / R'`, where `Map v` is the image of `v` under `j`.
|
LinearIndependent.injective_total
theorem LinearIndependent.injective_total :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M], LinearIndependent R v → Function.Injective ⇑(Finsupp.total ι M R v)
The theorem `LinearIndependent.injective_total` states that for any types `ι`, `R`, and `M`, and any function `v` from `ι` to `M`, given a structure of a ring on `R`, an additive commutative group structure on `M`, and a module structure over `R` on `M`, if the family of vectors `v` is linearly independent over `R`, then the function associated to the total function of the finitely supported function (Finsupp.total) applied to `v` is injective. In other words, this theorem connects the concept of linear independence with the injectivity of the total function in the context of a finitely supported function.
More concisely: If `v : ι → M` is a linearly independent family of vectors over a ring `R` with `M` being an additive commutative group and a module over `R`, then the total function `Finsupp.total v` is an injective function from `fin ι` to `M`.
|
LinearIndependent.units_smul
theorem LinearIndependent.units_smul :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{v : ι → M}, LinearIndependent R v → ∀ (w : ι → Rˣ), LinearIndependent R (w • v)
The theorem `LinearIndependent.units_smul` states that for any type `ι`, ring `R`, and additively commutative group `M` with `M` being a module over `R`, if a family of vectors `v` over `M` indexed by `ι` is linearly independent over `R`, then for any function `w` from `ι` to the multiplicative group of units in `R`, the family of vectors obtained by scaling each vector in `v` by the corresponding unit in `w` is also linearly independent over `R`. This theorem essentially means that scaling a set of linearly independent vectors by non-zero scalars does not affect their linear independence.
More concisely: If `{v i : M | i : ι}` is a linearly independent family of vectors over a ring `R` in an additively commutative group `M` that is an `R`-module, then scaling each vector `v i` by the corresponding unit `w i` in `R` results in a linearly independent family.
|
linearIndependent_equiv'
theorem linearIndependent_equiv' :
∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (e : ι ≃ ι') {f : ι' → M} {g : ι → M},
f ∘ ⇑e = g → (LinearIndependent R g ↔ LinearIndependent R f)
The theorem `linearIndependent_equiv'` states that for any types `ι` and `ι'`, a semiring `R`, and an add commutative monoid `M` that is also an `R`-module, given a bijection `e` from `ι` to `ι'`, and any functions `f` from `ι'` to `M` and `g` from `ι` to `M`, if `f` composed with `e` equals `g`, then `g` is linearly independent over `R` if and only if `f` is linearly independent over `R`. This theorem shows that the property of linear independence is preserved under change of indices of the vector, where the change of indices is performed via the given bijection.
More concisely: For any semiring R, add commutative monoid M as an R-module, bijection e between indices ι and ι', and functions f : ι' -> M and g : ι -> M with f ∘ e = g, the linear independence of f over R if and only if g is over R.
|
linearIndependent_iff'
theorem linearIndependent_iff' :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M],
LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), (s.sum fun i => g i • v i) = 0 → ∀ i ∈ s, g i = 0
The theorem `linearIndependent_iff'` states that for any semiring `R`, a set `v` of vectors from `ι` to `M`, an additively commutative monoid `M`, and a module `R M`, the set of vectors `v` is linearly independent over `R` if and only if for any finite set `s` of `ι` and any function `g` from `ι` to `R`, if the sum of the scalar multiples `g i • v i` for each `i` in `s` is zero, then `g i` must be zero for each `i` in `s`. In other words, a set of vectors is linearly independent if and only if no non-trivial linear combination of them equals zero.
More concisely: A set of vectors from a module over a semiring is linearly independent if and only if the sum of scalar multiples of vectors by any function from the set to the semiring is zero only when the function is the zero function.
|
LinearIndependent.map'
theorem LinearIndependent.map' :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'],
LinearIndependent R v → ∀ (f : M →ₗ[R] M'), LinearMap.ker f = ⊥ → LinearIndependent R (⇑f ∘ v)
The theorem `LinearIndependent.map'` states that for any type `ι`, semiring `R`, additive commutative monoids `M` and `M'`, and a function `v` from `ι` to `M`, if `v` is a linearly independent family of vectors over `R`, then any injective linear map `f` from `M` to `M'` sends `v` to another linearly independent family of vectors over `R`. In other words, the image of a linearly independent set under an injective linear map is also linearly independent. This theorem is a specific instance of the more general `LinearIndependent.map` theorem.
More concisely: A linearly independent family of vectors mapped by an injective linear transformation remains linearly independent.
|
linearIndependent_finset_map_embedding_subtype
theorem linearIndependent_finset_map_embedding_subtype :
∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
LinearIndependent (ι := { x // x ∈ s }) R Subtype.val → ∀ (t : Finset ↑s), LinearIndependent R Subtype.val
This theorem states that given a set `s` of elements of type `M`, if `s` is linearly independent over a semiring `R` (denoted by `LinearIndependent R Subtype.val`), then every finite subset `t` (of the subtype `↑s` where each element is in `s`) is also linearly independent over `R`. This is applicable for any types `R` and `M` where `R` is a semiring, `M` is an additive commutative monoid, and `M` is a module over `R`. In simpler words, every finite subset of a linearly independent set retains the property of linear independence.
More concisely: If a set of elements is linearly independent over a semiring, then every finite subset of the set is also linearly independent over the semiring.
|
LinearIndependent.map_of_surjective_injective
theorem LinearIndependent.map_of_surjective_injective :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {R' : Type u_8} {M' : Type u_9} [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M']
[inst_5 : Module R' M'],
LinearIndependent R v →
∀ (i : ZeroHom R R') (j : M →+ M'),
Function.Surjective ⇑i →
(∀ (m : M), j m = 0 → m = 0) → (∀ (r : R) (m : M), j (r • m) = i r • j m) → LinearIndependent R' (⇑j ∘ v)
The theorem states that for two modules `M / R` and `M' / R'`, if there is a surjective map `i : R → R'` that maps zero to zero, and a monoid map `j : M →+ M'` that sends non-zero elements to non-zero elements in such a way that the scalar multiplications on `M` and `M'` are compatible, then any linearly independent family of vectors in `M` under scalar multiplication by `R` is mapped to a linearly independent family of vectors in `M'` under scalar multiplication by `R'`. In other words, the map `j` preserves the property of linear independence. This can be seen as a generalized version of `LinearIndependent.map'` where `R = R'`.
More concisely: If `i : R → R'` is a surjective ring homomorphism mapping 0 to 0, and `j : M → M'` is a module homomorphism sending non-zero elements to non-zero elements with compatible scalar multiplications, then linearly independent families of `M` under scalar multiplication by `R` correspond to linearly independent families of `M'` under scalar multiplication by `R'`.
|
Fintype.linearIndependent_iff
theorem Fintype.linearIndependent_iff :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Fintype ι],
LinearIndependent R v ↔ ∀ (g : ι → R), (Finset.univ.sum fun i => g i • v i) = 0 → ∀ (i : ι), g i = 0
The theorem `Fintype.linearIndependent_iff` states that for any set of types `ι`, a semiring `R`, an additive commutative monoid `M`, and a function `v` from `ι` to `M`, given that `M` is a module over `R` and `ι` is finite, the family of vectors `v` is linearly independent over `R` if and only if for all functions `g` from `ι` to `R`, if the sum of `g i` scaled by `v i` over all elements `i` in the universal finite set is zero, then for all `i` in `ι`, `g i` must be equal to zero.
In mathematical terms, this means that a set of vectors is linearly independent if and only if no non-trivial linear combination of these vectors results in the zero vector.
More concisely: A family of vectors from a module over a semiring is linearly independent if and only if no non-zero, weighted sum of the vectors with coefficients from the semiring equals the zero vector, where the weights come from another function to the semiring.
|
LinearIndependent.linear_combination_pair_of_det_ne_zero
theorem LinearIndependent.linear_combination_pair_of_det_ne_zero :
∀ {R : Type u_8} {M : Type u_9} [inst : CommRing R] [inst_1 : NoZeroDivisors R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] {x y : M},
LinearIndependent R ![x, y] →
∀ {a b c d : R}, a * d - b * c ≠ 0 → LinearIndependent R ![a • x + b • y, c • x + d • y]
This theorem states that given a pair of linearly independent vectors `x` and `y` in a module `M` over a commutative ring `R` with no zero divisors, the vectors formed by their linear combinations `a * x + b * y` and `c * x + d * y` are also linearly independent, as long as the determinant `a*d - b*c` is not equal to zero. This theorem is a key part of understanding transformations and changes of basis in linear algebra.
More concisely: If `x` and `y` are linearly independent vectors in a module `M` over a commutative ring `R` with no zero divisors, then the vectors `a*x + b*y` and `c*x + d*y` are also linearly independent in `M` whenever `a*d - b*c` is nonzero.
|
exists_linearIndependent_extension
theorem exists_linearIndependent_extension :
∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V},
LinearIndependent (ι := { x // x ∈ s }) K Subtype.val →
s ⊆ t → ∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val
This theorem, `exists_linearIndependent_extension`, states that for any division ring `K` and any additive commutative group `V` that is a module over `K`, given two sets of vectors `s` and `t` from `V`, if `s` is a linearly independent set and is a subset of `t`, there exists a set `b` which is a subset of `t` such that `s` is a subset of `b`, `t` is a subset of the span of `b` over `K`, and `b` is a linearly independent set. In other words, it's possible to extend a linearly independent set `s` to another linearly independent set `b` that spans `t`.
More concisely: Given any division ring `K` and an additive commutative `K`-module `V`, if `s` is a linearly independent subset of `V` and `s` is contained in `t`, there exists a linearly independent subset `b` of `t` containing `s` such that `t` is contained in the span of `b` over `K`.
|
linearDependent_comp_subtype
theorem linearDependent_comp_subtype :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {s : Set ι},
¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔
∃ f ∈ Finsupp.supported R R s, (f.support.sum fun i => f i • v i) = 0 ∧ f ≠ 0
The theorem `linearDependent_comp_subtype` states that for any set `s` of indices `ι`, a semiring `R`, an additively commutative monoid `M`, and a family of vectors `v : ι → M` that forms a `R`-module, the family of vectors `v`, indexed over the subtype `↑s` and composed with the subtype value function, is not linearly independent if and only if there exists a function `f` in the `R`-submodule of all functions from `α` to `M` (denoted as `α →₀ M`) such that the support of `f` is a subset of `s`, where the sum of scalar multiplication of `f i` and `v i` over the support of `f` is zero and `f` is not the zero function.
In simpler terms, this theorem provides a condition to check if a subset of a family of vectors is linearly dependent. It states that a subset of vectors is linearly dependent if there exists a non-zero linear combination of them that sums up to zero.
More concisely: A subfamily of an R-module of vectors indexed by a set s is linearly dependent if and only if there exists a non-zero function in the R-submodule of all functions from a given algebraic structure to the module, whose support is a subset of s, and whose sum with the corresponding vectors is zero.
|
linearIndependent_empty
theorem linearIndependent_empty :
∀ (R : Type u_2) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
LinearIndependent R fun (x : ↑∅) => ↑x
The theorem `linearIndependent_empty` asserts that for any semiring `R` and any additive commutative monoid `M` that is also an `R`-module, the empty set of vectors is linearly independent over `R`. Essentially, this means there are no nontrivial linear combinations among the vectors in the empty set, which is trivially true as there are no vectors in the set.
More concisely: In any semiring `R` and additive commutative monoid `M` that is an `R`-module, the empty set of vectors is linearly independent over `R`.
|
LinearIndependent.fin_cons'
theorem LinearIndependent.fin_cons' :
∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : ℕ} (x : M)
(v : Fin m → M),
LinearIndependent R v →
(∀ (c : R) (y : ↥(Submodule.span R (Set.range v))), c • x + ↑y = 0 → c = 0) →
LinearIndependent R (Fin.cons x v)
This theorem, `LinearIndependent.fin_cons'`, states that for any semiring `R`, additively commutative monoid `M`, and a module structure over `R` and `M`, given a natural number `m`, an element `x` of `M` and a function `v` mapping from 'Fin m' to `M` (which can be thought of as a vector of `m` elements from `M`), if `v` is a linearly independent family of vectors and for any scalar `c` from `R` and vector `y` in the span of the range of `v`, the equation `c • x + y = 0` implies `c = 0`, then the function `Fin.cons x v` (which is a new family of vectors created by adding `x` at the beginning of `v`) is also a linearly independent family of vectors.
In other words, this theorem provides a condition under which prepending an element to a linearly independent vector will result in another linearly independent vector.
More concisely: Given a semiring `R`, additively commutative monoid `M` with a module structure over `R`, and a linearly independent family `v` of `m` elements in `M`, if for any scalar `c` from `R` and vector `y` in the span of `v`, the equation `c • x + y = 0` implies `c = 0` for all `x` in `{x | Fin.cons x v is a sub-vector of v}`, then `Fin.cons x v` is also a linearly independent family of vectors.
|
linearIndependent_fin_cons
theorem linearIndependent_fin_cons :
∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : 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)
The theorem `linearIndependent_fin_cons` states that for any division ring `K`, any additively commutative group `V`, any `K`-module `V`, any vector `x` from `V`, any natural number `n`, and any function `v` from a `n`-element finite type to `V`, the vectors defined by the function `Fin.cons x v` are linearly independent over `K` if and only if the vectors defined by `v` are linearly independent over `K` and the vector `x` is not in the span of the set of vectors given by the range of `v`. In simpler terms, it states that adding a new vector at the beginning of a linearly independent set of vectors will result in a linearly independent set if and only if the newly added vector is not a linear combination of the other vectors.
More concisely: Given a division ring K, an additively commutative group V, a K-module V, a vector x in V, a natural number n, and a function v from a n-element finite type to V, the vectors Fin.cons x v are linearly independent over K if and only if the vectors v are linearly independent over K and x is not in the span of v.
|
LinearIndependent.of_subtype_range
theorem LinearIndependent.of_subtype_range :
∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_8}
{f : ι → M},
Function.Injective f → LinearIndependent (ι := { x // x ∈ Set.range f }) R Subtype.val → LinearIndependent R f
This theorem, `LinearIndependent.of_subtype_range`, states that if we have a function `f : ι → M` that is injective and a set of vectors `Subtype.val` that are linearly independent over a semiring `R`, where `Subtype.val` is a subset of `M` consisting of elements in the range of `f`, then the function `f` is also linearly independent over the semiring `R`. Here `ι` and `M` are arbitrary types, `R` is a semiring, and `f` is a function from `ι` to `M`. Linear independence in this context means that no vector in the set can be represented as a linear combination of the other vectors from the same set.
More concisely: If `f : ι -> M` is an injective function and `{v : M | ∃ i : ι, v = Subtype.val i} \ included in Im f` is a linearly independent set of vectors over a semiring `R`, then `f` is a linearly independent function over `R`.
|
LinearIndependent.maximal_iff
theorem LinearIndependent.maximal_iff :
∀ {ι : Type w} {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] {M : Type v} [inst_2 : AddCommGroup M]
[inst_3 : 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
This theorem provides an alternative characterization of a maximal linearly independent family of vectors. A maximal linearly independent family is one that cannot be extended by adding more vectors while preserving linear independence. In terms of types, this theorem states that for a given linearly independent family `v` indexed by type `ι` and over a Ring `R` and a Module `M`, the family is maximal if and only if, for any other type `κ` and any other linearly independent family `w` indexed by `κ`, whenever there exists a function `j` from `ι` to `κ` such that `w` composed with `j` equals `v`, then `j` is a surjective function. In other words, every element of `κ` is the image of some element of `ι` under the function `j`.
More concisely: A linearly independent family of vectors over a ring in a module is maximal if and only if no other linearly independent family can be mapped to it via a surjective function.
|
LinearIndependent.fin_cons
theorem LinearIndependent.fin_cons :
∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V}
{n : ℕ} {v : Fin n → V},
LinearIndependent K v → x ∉ Submodule.span K (Set.range v) → LinearIndependent K (Fin.cons x v)
The theorem `LinearIndependent.fin_cons` states that for any division ring `K`, additively commutative group `V`, and module over `K` and `V`, given a vector `x` of `V`, a natural number `n`, and a function `v` mapping from `Fin n` to `V`, if the vectors generated by `v` are linearly independent over `K` and `x` is not in the span of the set of vectors generated by `v`, then the vectors generated by `Fin.cons x v`, which is obtained by adding `x` at the beginning of the `n`-tuple `v`, are also linearly independent over `K`.
More concisely: If a vector `x` is not in the span of linearly independent vectors `v_1, ..., v_n` in a module over a division ring `K`, then the vectors `x, v_1, ..., v_n` are also linearly independent in the module over `K`.
|
Fintype.linearIndependent_iff'
theorem Fintype.linearIndependent_iff' :
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
LinearIndependent R v ↔
LinearMap.ker ((LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.id.smulRight (v i)) = ⊥
The theorem `Fintype.linearIndependent_iff'` states that for any finite family of vectors `v i`, the vectors are linearly independent if and only if the linear map that maps each `c : ι → R` to the sum of `c i` scaled by `v i` (represented as `∑ i, c i • v i` in mathematical notation) has a trivial kernel. This is expressed in the context of a semiring `R` and an additively commutative monoid `M` which forms a module over `R`. The index set `ι` of the family is assumed to be a finite type, and the equality of indices is decidable.
More concisely: The finite family of vectors `{vi : M | i ∈ ι}` is linearly independent if and only if the kernel of the linear map that maps each function `c : ι → R` to the sum `∑ i, c i • vi` is the trivial subspace.
|