finrank_eq_one_iff
theorem finrank_eq_one_iff :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (ι : Type u_1)
[inst_3 : Unique ι], FiniteDimensional.finrank K V = 1 ↔ Nonempty (Basis ι K V)
This theorem states that, for any division ring `K` and additively commutative group `V` where `V` is a `K`-module and `ι` is a unique type, the finite rank of `V` over `K` is one if and only if there exists some `v` in `V` such that the singleton set `{v}` forms a basis for `V`. Here, the rank of a module is defined to be `0` if the module has infinite rank. In the context of a vector space `V` over a field `K`, this is equivalent to `V` having finite dimension `1` over `K`.
More concisely: For a division ring `K`, additively commutative group `V` being a `K`-module, and `ι` being a type, the module `V` has rank 1 over `K` if and only if there exists a basis consisting of a single element in `V`.
|
Subalgebra.bot_eq_top_of_rank_eq_one
theorem Subalgebra.bot_eq_top_of_rank_eq_one :
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] [inst_3 : Nontrivial E],
Module.rank F E = 1 → ⊥ = ⊤
This theorem, `Subalgebra.bot_eq_top_of_rank_eq_one`, states that for any given field `F` and ring `E` where `E` is an algebra over `F` and `E` is nontrivial, if the module rank of `E` over `F` is one, then the smallest possible subalgebra (`⊥`) is equivalent to the largest possible subalgebra (`⊤`). This is an alias of the reverse direction of `Subalgebra.bot_eq_top_iff_rank_eq_one`. In more casual terms, it asserts that if your algebraic structure is simple enough (i.e., it has rank one), then you can't get any smaller or larger than the whole thing.
More concisely: For any field `F` and nontrivial algebra `E` over `F` of rank one, the smallest and largest subalgebras of `E` are equivalent.
|
LinearMap.finiteDimensional_of_surjective
theorem LinearMap.finiteDimensional_of_surjective :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : FiniteDimensional K V] (f : V →ₗ[K] V₂),
LinearMap.range f = ⊤ → FiniteDimensional K V₂
This theorem states that if we have a surjective (onto) linear map `f` from a finite-dimensional vector space `V` over a division ring `K` into another vector space `V₂` over the same division ring, then the target space `V₂` is also finite-dimensional. Specifically, surjectivity in this context is expressed by the condition that the range of `f` equals the entire target space `V₂` (denoted `⊤`).
More concisely: If `f` is a surjective linear map from the finite-dimensional vector space `V` over division ring `K` to another finite-dimensional vector space `V₂` over the same division ring, then `V₂` is finite-dimensional.
|
finrank_eq_one_iff_of_nonzero
theorem finrank_eq_one_iff_of_nonzero :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V),
v ≠ 0 → (FiniteDimensional.finrank K V = 1 ↔ Submodule.span K {v} = ⊤)
The theorem `finrank_eq_one_iff_of_nonzero` states that for all division rings `K` and additively commutative groups `V` that form a module over `K`, given a non-zero vector `v` in `V`, the rank (or dimension) of `V` is 1 if and only if the vector `v` spans the entire space `V`. In other words, a vector space has dimension 1 if and only if a single non-zero vector spans the whole space. This can be seen intuitively: a single non-zero vector can only span a one-dimensional space.
More concisely: For a division ring K and an additively commutative K-module V, the vector v in V is a spanning set if and only if the rank of V equals 1.
|
FiniteDimensional.finrank_eq_rank'
theorem FiniteDimensional.finrank_eq_rank' :
∀ (K : Type u) (V : Type v) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V], ↑(FiniteDimensional.finrank K V) = Module.rank K V
This theorem states that in a finite-dimensional vector space, the dimension of the space seen as a natural number (or 'finrank') is equivalent to its dimension seen as a cardinal number (or 'rank'). This fact holds for any vector space `V` over a division ring `K`. The significance of this theorem is it enables easier searches in the typeclass system in Lean 4, and it makes a connection between two ways of measuring the 'size' or dimensionality of a vector space.
More concisely: In a finite-dimensional vector space over a division ring, the rank (as a cardinal number) equals the finite rank (as a natural number).
|
LinearMap.surjective_of_injective
theorem LinearMap.surjective_of_injective :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {f : V →ₗ[K] V}, Function.Injective ⇑f → Function.Surjective ⇑f
This theorem states that in a finite-dimensional vector space, any linear map that is injective (i.e., it assigns a unique output to every input) is also surjective (i.e., every point in the vector space is mapped to by some vector). Specifically, if we have a vector space `V` over a division ring `K`, and a linear map `f` from `V` to `V` (expressed as `f : V →ₗ[K] V`), then if `f` is injective (`Function.Injective ⇑f` meaning that for all distinct vectors in `V`, their images under `f` are also distinct), it must also be surjective (`Function.Surjective ⇑f` meaning that for every vector in `V`, there exists another vector that when transformed by `f` results in that vector).
More concisely: In a finite-dimensional vector space over a division ring, an injective linear map is surjective.
|
FiniteDimensional.span_of_finite
theorem FiniteDimensional.span_of_finite :
∀ (K : Type u) {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {A : Set V},
A.Finite → FiniteDimensional K ↥(Submodule.span K A)
The theorem `FiniteDimensional.span_of_finite` states that for any division ring `K`, any additive commutative group `V` that is also a `K`-module, and any finite set `A` of elements from `V`, the submodule generated by `A` (i.e., the smallest submodule that contains `A`) is finite-dimensional. In other words, if we have a finite set in a vector space, the vector space spanned by this set (i.e., the set of all linear combinations of the vectors in this set) is a finite-dimensional vector space.
More concisely: For any division ring K, any finite subset A of a K-module V, the submodule generated by A is finite-dimensional.
|
Submodule.finrank_lt_finrank_of_lt
theorem Submodule.finrank_lt_finrank_of_lt :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{s t : Submodule K V} [inst_3 : FiniteDimensional K ↥t],
s < t → FiniteDimensional.finrank K ↥s < FiniteDimensional.finrank K ↥t
This theorem states that for any division ring `K` and an additive commutative group `V` that forms a module over `K`, if `s` and `t` are submodules of `V` such that `t` is of finite dimension and `s` is strictly smaller than `t`, then the rank (or the dimension in the finite case) of `s` is strictly less than the rank of `t`. Here, `<` denotes the proper subset relation between submodules and not a numerical comparison.
More concisely: If `K` is a division ring, `V` is an additive commutative `K`-module, `s` and `t` are submodules of `V` with `t` finite-dimensional and `s` a proper submodule of `t`, then the dimension of `s` is strictly less than the dimension of `t`.
|
LinearEquiv.finiteDimensional
theorem LinearEquiv.finiteDimensional :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂],
(V ≃ₗ[K] V₂) → ∀ [inst_5 : FiniteDimensional K V], FiniteDimensional K V₂
The theorem `LinearEquiv.finiteDimensional` states that the property of being a finite-dimensional vector space is preserved under a linear equivalence. Specifically, given a division ring `K` and two vector spaces `V` and `V₂` over `K`, if `V` is a finite-dimensional vector space and there exists a linear equivalence (i.e., a bijective linear transformation) between `V` and `V₂`, then `V₂` is also a finite-dimensional vector space.
More concisely: If two finite-dimensional vector spaces over a division ring are linearly equivalent, then they have equal finite dimensions.
|
LinearMap.comp_eq_id_comm
theorem LinearMap.comp_eq_id_comm :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {f g : V →ₗ[K] V}, f ∘ₗ g = LinearMap.id ↔ g ∘ₗ f = LinearMap.id
In the context of finite-dimensional vector spaces over a division ring, the theorem states that for any two linear maps `f` and `g` from the vector space to itself, the composition `f ∘ₗ g` equals the identity map if and only if the composition `g ∘ₗ f` equals the identity map. In other words, if `f` and `g` are one-sided inverses of each other in one direction, they must also be one-sided inverses in the other direction.
More concisely: The two linear maps `f` and `g` from a finite-dimensional vector space over a division ring are mutual one-sided inverses if and only if both `f ∘ₗ g` and `g ∘ₗ f` equal the identity map.
|
finrank_span_singleton
theorem finrank_span_singleton :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {v : V},
v ≠ 0 → FiniteDimensional.finrank K ↥(Submodule.span K {v}) = 1
This theorem states that for any division ring `K` and an additive commutative group `V` that is also a `K`-module, if `v` is a non-zero element of `V`, then the rank of the submodule of `V` generated (or spanned) by the singleton set `{v}` is `1`. In other words, the dimension of the vector space spanned by a single non-zero vector is `1`.
More concisely: For any division ring K and additive commutative group V being a K-module, the dimension of the subspace spanned by a non-zero element in V is 1.
|
FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card
theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card :
∀ {L : Type u_1} [inst : LinearOrderedField L] {W : Type v} [inst_1 : AddCommGroup W] [inst_2 : Module L W]
[inst_3 : FiniteDimensional L W] {t : Finset W},
FiniteDimensional.finrank L W + 1 < t.card →
∃ f, (t.sum fun e => f e • e) = 0 ∧ (t.sum fun e => f e) = 0 ∧ ∃ x ∈ t, 0 < f x
This theorem is a strengthened version of `exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card`, applicable when working over an ordered field. Given a finite dimensional vector space `W` over a linear ordered field `L`, and a finite set `t` of vectors in `W`, the theorem states that if the rank (or dimension) of `W` plus one is strictly less than the cardinality of `t`, then there exists a function `f` such that the sum of `f(e) * e` over all `e` in `t` equals zero, the sum of `f(e)` over all `e` in `t` also equals zero, and there is some `x` in `t` for which `f(x)` is positive. Essentially, we can find a nontrivial linear relation among vectors in `t` where at least one of the coefficients is positive.
More concisely: Given a finite-dimensional vector space over an ordered field with strictly fewer dimensions than the number of vectors, there exists a linear relation among these vectors with at least one positive coefficient summing to zero.
|
finrank_eq_one_iff'
theorem finrank_eq_one_iff' :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
FiniteDimensional.finrank K V = 1 ↔ ∃ v, v ≠ 0 ∧ ∀ (w : V), ∃ c, c • v = w
This theorem states that for any division ring `K` and any module `V` over `K`, the module has a finite dimension of 1 if and only if there exists some non-zero vector `v` in `V` such that every vector in `V` can be expressed as a multiple of `v`. In other words, the entire module `V` can be generated by a single non-zero vector.
More concisely: A module of finite dimension 1 over a division ring is generated by a single non-zero vector.
|
LinearMap.mul_eq_one_comm
theorem LinearMap.mul_eq_one_comm :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {f g : V →ₗ[K] V}, f * g = 1 ↔ g * f = 1
This theorem states that, in a finite-dimensional vector space over a division ring, for any two linear maps `f` and `g` from the vector space to itself, the condition that the composition of `f` and `g` equals the identity map is equivalent to the condition that the composition of `g` and `f` equals the identity map. In simpler terms, if `f` followed by `g` gives the identity, then `g` followed by `f` also gives the identity, and vice versa. This property is specific to finite-dimensional spaces and doesn't generally hold in infinite-dimensional spaces.
More concisely: In a finite-dimensional vector space over a division ring, the composition of `f` and `g` equals the identity map if and only if the composition of `g` and `f` equals the identity map.
|
Subalgebra.bot_eq_top_of_finrank_eq_one
theorem Subalgebra.bot_eq_top_of_finrank_eq_one :
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] [inst_3 : Nontrivial E],
FiniteDimensional.finrank F E = 1 → ⊥ = ⊤
This theorem, named `Subalgebra.bot_eq_top_of_finrank_eq_one`, states that for any field `F` and any ring `E` that has an algebra structure over `F` and is nontrivial, if the rank of `E` over `F` as a finite dimensional space is equal to one, then the smallest subalgebra (denoted as `⊥`) is equal to the largest subalgebra (denoted as `⊤`). In other words, if a nontrivial algebra over a field has a finite rank of one, it is comprised of a single subalgebra, which is both the smallest and largest possible subalgebra.
More concisely: For any nontrivial field extension F and finite-dimensional algebra E over F, if the rank of E over F is equal to 1, then the smallest and largest subalgebras of E are equal.
|
FiniteDimensional.of_finrank_eq_succ
theorem FiniteDimensional.of_finrank_eq_succ :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ},
FiniteDimensional.finrank K V = n.succ → FiniteDimensional K V
This theorem states that for any division ring `K` and any additively commutative group `V` that is also a module over `K`, if the rank of `V` as a `K`-module (expressed as a natural number) is equal to the successor of another natural number `n`, then `V` is a finite-dimensional vector space over `K`. In other words, if the finite rank of the module `V` over `K` is `n+1`, then `V` is finite-dimensional over `K`.
More concisely: If a module over a division ring has finite rank equal to the successor of a natural number, then it is finite-dimensional.
|
FiniteDimensional.lt_aleph0_of_linearIndependent
theorem FiniteDimensional.lt_aleph0_of_linearIndependent :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type w}
[inst_3 : FiniteDimensional K V] {v : ι → V}, LinearIndependent K v → Cardinal.mk ι < Cardinal.aleph0
This theorem, named `FiniteDimensional.lt_aleph0_of_linearIndependent`, states that for any division ring `K` and additively commutative group `V` forming a module, together with any finite-dimensional vector space over `K` and `V` and any function `v` from an index set `ι` to `V` that generates a linearly independent set, the cardinality of the index set `ι` is strictly less than `ℵ₀` (aleph zero), the smallest infinite cardinal number. In other words, in a finite-dimensional vector space, any set of linearly independent vectors must be finite and of cardinality less than the smallest infinite cardinal number.
More concisely: In a finite-dimensional vector space over a division ring, every linearly independent set has finite and strictly smaller cardinality than the first infinite cardinal number.
|
Submodule.finiteDimensional_of_le
theorem Submodule.finiteDimensional_of_le :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S₁ S₂ : Submodule K V} [inst_3 : FiniteDimensional K ↥S₂], S₁ ≤ S₂ → FiniteDimensional K ↥S₁
This theorem states that if you have a submodule that is contained within another submodule, and the containing submodule is finite-dimensional, then the contained submodule is also finite-dimensional. In more technical terms, given two submodules `S₁` and `S₂` of a module `V` over a division ring `K`, if `S₂` is finite-dimensional and `S₁` is a subset of `S₂`, then `S₁` is also finite-dimensional.
More concisely: If a finite-dimensional submodule contains another submodule, then the contained submodule is also finite-dimensional.
|
Submodule.finrank_quotient_add_finrank
theorem Submodule.finrank_quotient_add_finrank :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] (s : Submodule K V),
FiniteDimensional.finrank K (V ⧸ s) + FiniteDimensional.finrank K ↥s = FiniteDimensional.finrank K V
The theorem `Submodule.finrank_quotient_add_finrank` states that for any given division ring `K` and a finite-dimensional vector space `V` over `K`, with a submodule `s` of `V`, the sum of the dimensions (as natural numbers) of the quotient space `V/s` and the submodule `s` is equal to the dimension of the vector space `V`. This theorem is an analogue in the language of modules and division rings of the rank-nullity theorem for linear maps in linear algebra.
More concisely: The sum of the dimensions of a finite-dimensional vector space and its submodule equals the dimension of the vector space.
|
LinearMap.mul_eq_one_of_mul_eq_one
theorem LinearMap.mul_eq_one_of_mul_eq_one :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {f g : V →ₗ[K] V}, f * g = 1 → g * f = 1
The theorem `LinearMap.mul_eq_one_of_mul_eq_one` states that in a finite-dimensional vector space, if we have two linear maps `f` and `g` such that the composition of `f` followed by `g` is the identity map (i.e., `f * g = 1`), then the composition of `g` followed by `f` is also the identity map (i.e., `g * f = 1`). This property holds for any finite-dimensional vector space over a division ring `K`.
More concisely: In a finite-dimensional vector space over a division ring, if the composition of two linear maps is equal to the identity map, then their compositions in the reverse order are also equal to the identity map.
|
Subalgebra.eq_of_le_of_finrank_eq
theorem Subalgebra.eq_of_le_of_finrank_eq :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Ring L] [inst_2 : Algebra K L] {F E : Subalgebra K L}
[hfin : FiniteDimensional K ↥E],
F ≤ E → FiniteDimensional.finrank K ↥F = FiniteDimensional.finrank K ↥E → F = E
This theorem states that if we have a subalgebra `F` contained in another subalgebra `E` over a field `K`, with `E` being a finite-dimensional vector space, then `F` and `E` are equal if they have the same finite dimension. The condition that `F` is contained in `E` is denoted `F ≤ E` in the theorem, and `FiniteDimensional.finrank K ↥F = FiniteDimensional.finrank K ↥E` represents that `F` and `E` have the same finite dimension.
More concisely: If `F` is a subalgebra of `E`, both contained in a field `K`, and have equal finite dimension, then `F = E`.
|
FiniteDimensional.of_fintype_basis
theorem FiniteDimensional.of_fintype_basis :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type w}
[inst_3 : Finite ι], Basis ι K V → FiniteDimensional K V
The theorem `FiniteDimensional.of_fintype_basis` states that if a vector space has a basis that is finite, then the vector space is finite-dimensional. Here, `K` is a division ring, `V` is an additive commutative group with a module structure over `K`, and `ι` is the type indexing the basis of the vector space. The basis is represented as a function from `ι` to `V`. If `ι` is finite (i.e., there are finitely many basis vectors), then the vector space is considered finite-dimensional.
More concisely: If a vector space over a division ring with a finite basis is given, then the vector space is finite-dimensional.
|
FiniteDimensional.of_subalgebra_toSubmodule
theorem FiniteDimensional.of_subalgebra_toSubmodule :
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] {S : Subalgebra F E},
FiniteDimensional F ↥(Subalgebra.toSubmodule S) → FiniteDimensional F ↥S
The theorem `FiniteDimensional.of_subalgebra_toSubmodule` states that for any field `F`, ring `E`, and `S` as a subalgebra from `E` over `F`, if the submodule associated with the subalgebra `S` is finite-dimensional over `F`, then the subalgebra `S` itself is also finite-dimensional over `F`. In simpler terms, it states that if the set of elements of a subalgebra forms a finite-dimensional submodule, then the subalgebra is finite-dimensional.
More concisely: If a subalgebra of a ring is a finite-dimensional submodule over its field of coefficients, then the subalgebra is finite-dimensional.
|
Subalgebra.finrank_eq_one_iff
theorem Subalgebra.finrank_eq_one_iff :
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] [inst_3 : Nontrivial E]
{S : Subalgebra F E}, FiniteDimensional.finrank F ↥S = 1 ↔ S = ⊥
This theorem states that for any field `F`, any ring `E` that has an algebra structure over `F`, and any nontrivial subalgebra `S` of `E`, the rank of `S` as a `F`-module being equal to 1 is equivalent to `S` being the bottom (i.e., zero) subalgebra. In other words, a subalgebra of a ring over a field has rank one if and only if it is the zero subalgebra. This is calculated in terms of the finiteness of the dimension of the module, which is a natural number defined as zero if the space has infinite rank.
More concisely: A subalgebra of a ring over a field has rank 1 as an `F`-module if and only if it is the zero subalgebra.
|
basisOfLinearIndependentOfCardEqFinrank.proof_1
theorem basisOfLinearIndependentOfCardEqFinrank.proof_1 :
∀ {K : Type u_2} {V : Type u_1} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{ι : Type u_3} [inst_3 : Nonempty ι] [inst_4 : Fintype ι] {b : ι → V},
LinearIndependent K b → Fintype.card ι = FiniteDimensional.finrank K V → ⊤ ≤ Submodule.span K (Set.range b)
This theorem states that for any division ring 'K' and an additively commutative group 'V' that forms a module over 'K', given a type 'ι' that is nonempty and finite, and a function 'b' from 'ι' to 'V', if the set of vectors 'b' is linearly independent over 'K' and the number of elements in 'ι' equals the rank of the module 'V' over 'K', then the total (or universal) submodule is less than or equal to the submodule spanned by the range of 'b'. In other words, the span of the range of this linearly independent function 'b' covers the entire module 'V', when the cardinality of 'ι' matches the rank of 'V'.
More concisely: If 'V' is an additively commutative 'K'-module of finite rank, and 'b' is a function from a finite, nonempty set 'ι' to 'V' such that the set of vectors {b i | i ∈ ι} is linearly independent over 'K', then the submodule generated by 'b' ('span {b i | i ∈ ι}') contains the whole module 'V'.
|
FiniteDimensional.of_rank_eq_one
theorem FiniteDimensional.of_rank_eq_one :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Module.rank K V = 1 → FiniteDimensional K V
This theorem states that for any given division ring `K` and any additively commutative group `V` that is a `K`-module, if the rank of the module `V` over the ring `K` is equal to `1`, then `V` is a finite-dimensional vector space over `K`. In other words, if a `K`-module `V` can be generated by a single element, then it forms a finite-dimensional vector space.
More concisely: If a one-dimensional `K`-module `V` over a division ring `K` is an additively commutative group, then `V` is a finite-dimensional vector space over `K`.
|
Submodule.finrank_lt
theorem Submodule.finrank_lt :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {s : Submodule K V},
s < ⊤ → FiniteDimensional.finrank K ↥s < FiniteDimensional.finrank K V
This theorem states that for any strict submodule `s` of a vector space `V` over a field `K`, where `V` is a finite dimensional space, the dimension (or rank) of the submodule `s` is strictly less than the dimension of the space `V`. Here, a 'strict submodule' means a submodule that is not equal to the whole space (`s < ⊤`). In mathematical terms, if `V` is a finite dimensional vector space over a field `K`, and `s` is a proper subspace of `V`, then the dimension of `s` is strictly less than the dimension of `V`.
More concisely: For any finite dimensional vector space V over a field K, the dimension of a strict submodule s is strictly less than the dimension of V.
|
FiniteDimensional.of_surjective
theorem FiniteDimensional.of_surjective :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂),
Function.Surjective ⇑f → ∀ [inst_5 : FiniteDimensional K V], FiniteDimensional K V₂
The theorem `FiniteDimensional.of_surjective` states that if we have a surjective linear map `f` from a vector space `V` to another vector space `V₂` over the same division ring `K`, and if `V` is finite-dimensional, then `V₂` must also be finite-dimensional. In other words, the surjectivity of the linear map and the finiteness of the dimension of the domain vector space ensure the finiteness of the dimension of the codomain vector space.
More concisely: If `V` is a finite-dimensional vector space over a division ring `K` and `f : V → V₂` is a surjective linear map, then `V₂` is also finite-dimensional.
|
finrank_le_one_iff
theorem finrank_le_one_iff :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V], FiniteDimensional.finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w
The theorem `finrank_le_one_iff` states that for any finite dimensional module, denoted `V`, over a division ring, denoted `K`, the rank (or dimension) of the module is less than or equal to 1 if and only if there exists some vector `v` in `V` such that every vector in `V` is a scalar multiple of `v`. In other words, all vectors in `V` can be expressed as `c • v = w`, where `c` is a scalar from `K`, `v` and `w` are vectors in `V`, and `•` denotes scalar multiplication. The condition of having rank at most 1 is equivalent to `V` being spanned by a single vector.
More concisely: The rank of a finite dimensional module over a division ring is at most 1 if and only if the module is spanned by a single vector.
|
FiniteDimensional.eq_of_le_of_finrank_eq
theorem FiniteDimensional.eq_of_le_of_finrank_eq :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S₁ S₂ : Submodule K V} [inst_3 : FiniteDimensional K ↥S₂],
S₁ ≤ S₂ → FiniteDimensional.finrank K ↥S₁ = FiniteDimensional.finrank K ↥S₂ → S₁ = S₂
The theorem `FiniteDimensional.eq_of_le_of_finrank_eq` states that for any given division ring `K` and an additive commutative group `V` that forms a module with `K`, if we consider two submodules `S₁` and `S₂` of this module such that `S₁` is contained in `S₂` (`S₁ ≤ S₂`) and `S₂` is a finite-dimensional submodule, if `S₁` and `S₂` have the same finite rank (dimension), then `S₁` and `S₂` are identical (`S₁ = S₂`). This can be interpreted as a theorem stating that in a finite-dimensional vector space, any subspace that is contained within another subspace and has the same dimension as the containing subspace must be equal to the containing subspace.
More concisely: In a finite-dimensional module over a division ring, two submodules with equal rank and one contained in the other are identical.
|
FiniteDimensional.of_finrank_pos
theorem FiniteDimensional.of_finrank_pos :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
0 < FiniteDimensional.finrank K V → FiniteDimensional K V
This theorem states that for any type `K` which is a Division Ring, and any type `V` that forms an Additive Commutative Group and a Module over `K`, if the rank of the Module `V` over the Ring `K` is greater than zero (i.e., it is not a zero-dimensional space), then `V` is a Finite Dimensional Vector Space over `K`. It formalizes the intuition that any non-zero dimensional space must indeed have a finite number of dimensions, in the context of vector spaces over a field.
More concisely: If `K` is a division ring and `V` is an additive commutative group of type `Type` that is a module over `K` with positive rank, then `V` is a finite-dimensional vector space over `K`.
|
Subalgebra.finiteDimensional_toSubmodule
theorem Subalgebra.finiteDimensional_toSubmodule :
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] {S : Subalgebra F E},
FiniteDimensional F ↥(Subalgebra.toSubmodule S) ↔ FiniteDimensional F ↥S
This theorem states that for any field `F` and ring `E` with an algebra structure, and any subalgebra `S` of `E` over `F`, the subalgebra `S` is finite-dimensional if and only if it is finite-dimensional when considered as a submodule. In other words, `S` has a finite basis as a vector space over `F` if and only if it also has a finite basis when viewed as a submodule of `E`.
More concisely: For any field `F`, ring `E` with an algebra structure, and subalgebra `S` of `E` over `F`, `S` is finite-dimensional as a vector space over `F` if and only if it is finite-dimensional as a submodule of `E`.
|
LinearMap.injective_iff_surjective
theorem LinearMap.injective_iff_surjective :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {f : V →ₗ[K] V}, Function.Injective ⇑f ↔ Function.Surjective ⇑f
This theorem states that for any finite-dimensional vector space over a division ring, a linear map on that space is injective if and only if it is surjective. In other words, in such a space, if a linear map never maps different vectors to the same vector (injectivity), then it must map some vector to every possible vector in the space (surjectivity), and vice versa.
More concisely: In a finite-dimensional vector space over a division ring, a linear map is both injective and surjective if and only if it is bijective.
|
LinearMap.finrank_range_add_finrank_ker
theorem LinearMap.finrank_range_add_finrank_ker :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : FiniteDimensional K V] (f : V →ₗ[K] V₂),
FiniteDimensional.finrank K ↥(LinearMap.range f) + FiniteDimensional.finrank K ↥(LinearMap.ker f) =
FiniteDimensional.finrank K V
The theorem `LinearMap.finrank_range_add_finrank_ker` is a statement of the Rank-Nullity Theorem in the context of linear maps and finite-dimensional vector spaces. It states that for any given division ring `K`, vector spaces `V` and `V₂` over `K`, and a linear map `f` from `V` to `V₂`, the sum of the dimensions of the range and the kernel of the linear map `f` is equal to the dimension of the source vector space `V`. Here, the dimension of a vector space is referred to as its 'rank', and is represented by the `FiniteDimensional.finrank` function. The kernel of a map is the set of all elements which map to zero, and the range is the set of all possible outputs of the map.
More concisely: The rank of a linear map from a finite-dimensional vector space equals the sum of the dimensions of its kernel and range.
|
finrank_eq_one_iff_of_nonzero'
theorem finrank_eq_one_iff_of_nonzero' :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V),
v ≠ 0 → (FiniteDimensional.finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w)
The theorem `finrank_eq_one_iff_of_nonzero'` states that for any division ring `K` and any module `V` over `K`, with `v` as a nonzero vector in `V`, the dimension (rank) of the module `V` is `1` if and only if every vector in `V` can be expressed as a scalar multiple of `v`. Here, scalar multiplication is denoted by `c • v`, where `c` is a scalar in `K`. So, in other words, `V` is one-dimensional if and only if it is spanned by a single, non-zero vector `v`.
More concisely: The module V over a division ring K has dimension 1 if and only if every vector in V can be expressed as a scalar multiple of a fixed non-zero vector v in V.
|
exists_smul_eq_of_finrank_eq_one
theorem exists_smul_eq_of_finrank_eq_one :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
FiniteDimensional.finrank K V = 1 → ∀ {x : V}, x ≠ 0 → ∀ (y : V), ∃ c, c • x = y
The theorem `exists_smul_eq_of_finrank_eq_one` states that in a one-dimensional vector space `V` over a division ring `K`, any vector `y` in `V` can be expressed as a scalar multiple of any non-zero vector `x` in `V`. This means if `x` is a non-zero vector and `y` is any vector in `V`, then there exists a scalar `c` in `K` such that `c * x = y`. The assumption that the vector space is one-dimensional is expressed by the condition `FiniteDimensional.finrank K V = 1`.
More concisely: In a one-dimensional vector space over a division ring, any vector can be expressed as a scalar multiple of any non-zero vector.
|
Subalgebra.eq_of_le_of_finrank_le
theorem Subalgebra.eq_of_le_of_finrank_le :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Ring L] [inst_2 : Algebra K L] {F E : Subalgebra K L}
[hfin : FiniteDimensional K ↥E],
F ≤ E → FiniteDimensional.finrank K ↥E ≤ FiniteDimensional.finrank K ↥F → F = E
This theorem states that if one subalgebra, `F`, is contained within another finite-dimensional subalgebra, `E`, with the same or smaller dimension (dimension denoted by `FiniteDimensional.finrank`), then those two subalgebras are actually equal. This applies to any Field `K` and Ring `L` where `L` is an algebra over `K`, and where `E` is a finite-dimensional algebra. The conclusion of equality between `F` and `E` follows from the combination of `F` being a subset of `E` and the dimension of `E` being less than or equal to the dimension of `F`.
More concisely: If `F` is a subalgebra of finite-dimensional algebra `E` over field `K` with the same or smaller dimension, then `F` is equal to `E`.
|
FiniteDimensional.of_injective
theorem FiniteDimensional.of_injective :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
[inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂),
Function.Injective ⇑f → ∀ [inst_5 : FiniteDimensional K V₂], FiniteDimensional K V
The theorem `FiniteDimensional.of_injective` states that for any division ring `K` and any two types `V` and `V₂` equipped with the structure of `K`-modules (that is, vector spaces over `K`), if there exists a `K`-linear map `f : V →ₗ[K] V₂` that is injective (i.e., no two different points in `V` get mapped to the same point in `V₂`), then if `V₂` is finite-dimensional (i.e., there exists a finite basis for the vector space `V₂`), it implies that `V` is also finite-dimensional. In simpler terms, the injective linear map from a vector space to a finite-dimensional vector space can't have an infinite-dimensional domain.
More concisely: If `K` is a division ring and `f : V → V₂` is an injective `K`-linear map between `K`-modules `V` and `V₂`, and `V₂` is finite-dimensional, then `V` is also finite-dimensional.
|
Submodule.eq_top_of_finrank_eq
theorem Submodule.eq_top_of_finrank_eq :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {S : Submodule K V},
FiniteDimensional.finrank K ↥S = FiniteDimensional.finrank K V → S = ⊤
The theorem `Submodule.eq_top_of_finrank_eq` states that if a submodule of a finite dimensional space has the same dimension (rank) as the whole space, then the submodule is, in fact, the entire space itself. Here, `K` denotes a division ring, `V` is an additive commutative group which is also a `K`-module, and `S` is a submodule of `V`. The theorem states that if the rank of `S` (given by `FiniteDimensional.finrank K ↥S`) is equal to the rank of `V` (given by `FiniteDimensional.finrank K V`), then `S` is equal to the entire space, denoted by `⊤` in Lean.
More concisely: If two finite dimensional subspaces of a vector space over a division ring have the same rank, then they are equal.
|
Submodule.finrank_sup_add_finrank_inf_eq
theorem Submodule.finrank_sup_add_finrank_inf_eq :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(s t : Submodule K V) [inst_3 : FiniteDimensional K ↥s] [inst_4 : FiniteDimensional K ↥t],
FiniteDimensional.finrank K ↥(s ⊔ t) + FiniteDimensional.finrank K ↥(s ⊓ t) =
FiniteDimensional.finrank K ↥s + FiniteDimensional.finrank K ↥t
The theorem 'Submodule.finrank_sup_add_finrank_inf_eq' asserts that for any division ring 'K' and additively commutative group 'V' with a 'K'-module structure, and for any two submodules 's' and 't' of 'V' which are finite-dimensional over 'K', the sum of the dimensions of the supremum (join) of 's' and 't' and the infimum (meet) of 's' and 't' is equal to the sum of the dimensions of 's' and 't'. In mathematical terms, this can be written as $\dim_K(s \vee t) + \dim_K(s \wedge t) = \dim_K(s) + \dim_K(t)$, where $\dim_K$ denotes the dimension over 'K', $\vee$ denotes the supremum (or the smallest submodule containing both 's' and 't'), and $\wedge$ denotes the infimum (or the largest submodule contained in both 's' and 't').
More concisely: For any finite-dimensional submodules $s$ and $t$ of a $K$-module $V$, the dimension of their join (supremum) plus the dimension of their meet (infimum) equals the sum of their dimensions: $\dim_K(s \vee t) + \dim_K(s \wedge t) = \dim_K(s) + \dim_K(t)$.
|
FiniteDimensional.of_finite_basis
theorem FiniteDimensional.of_finite_basis :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type w}
{s : Set ι}, Basis (↑s) K V → s.Finite → FiniteDimensional K V
This theorem states that if a vector space has a basis which is indexed by elements of a finite set, then the vector space is finite-dimensional. Here, `K` is the field over which the vector space `V` is defined, `ι` is the index type, and `s` is a finite set of indices. The statement `Basis (↑s) K V` confirms that the basis of the vector space `V` over the field `K` is indexed by elements of the set `s`. The condition `s.Finite` asserts that `s` is a finite set. The conclusion `FiniteDimensional K V` declares that the vector space `V` is finite-dimensional over the field `K`.
More concisely: If a vector space over a field has a finite basis, then it is finite-dimensional.
|
Submodule.fg_iff_finiteDimensional
theorem Submodule.fg_iff_finiteDimensional :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(s : Submodule K V), s.FG ↔ FiniteDimensional K ↥s
This theorem states that for any given submodule `s` of a vector space `V` over a division ring `K`, `s` is finitely generated if and only if it is finite-dimensional. In other words, a submodule has a finite set of generators that spans it if and only if it has a finite basis.
More concisely: A submodule of a vector space is finitely generated if and only if it is finite-dimensional.
|
is_simple_module_of_finrank_eq_one
theorem is_simple_module_of_finrank_eq_one :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {A : Type u_1}
[inst_3 : Semiring A] [inst_4 : Module A V] [inst_5 : SMul K A] [inst_6 : IsScalarTower K A V],
FiniteDimensional.finrank K V = 1 → IsSimpleOrder (Submodule A V)
This theorem states that for any module `V` over a `K`-algebra `A` where `K` is a division ring, if `V` is 1-dimensional over `K`, then `V` is a simple module. Here, simplicity of a module means that it has no proper non-zero submodules. The dimensionality of `V` over `K` is defined by the function `FiniteDimensional.finrank K V`, and a value of `1` indicates that `V` is 1-dimensional. The condition `IsScalarTower K A V` ensures that scalar multiplication in `V` is compatible with the ring operations in `K` and `A`.
More concisely: If `V` is a `1`-dimensional module over a `K`-algebra `A` where `K` is a division ring, then `V` is a simple module. (A module `V` is simple if it has no proper non-zero submodules.)
|
FiniteDimensional.subalgebra_toSubmodule
theorem FiniteDimensional.subalgebra_toSubmodule :
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] {S : Subalgebra F E},
FiniteDimensional F ↥S → FiniteDimensional F ↥(Subalgebra.toSubmodule S)
The theorem `FiniteDimensional.subalgebra_toSubmodule` states that for any field `F` and ring `E` with an algebra structure over `F`, and any subalgebra `S` of `E`, if `S` is a finite-dimensional vector space over `F`, then the corresponding submodule of `S` (obtained by forgetting some algebra structure via the map `Subalgebra.toSubmodule`) is also a finite-dimensional vector space over `F`. In other words, a subalgebra's finite-dimensionality is preserved when viewed as a submodule.
More concisely: If `F` is a field, `E` is a ring with an algebra structure over `F`, `S` is a finite-dimensional subalgebra of `E`, then the submodule of `S` in `E` (obtained by forgetting the algebra structure) is also a finite-dimensional vector space over `F`.
|
FiniteDimensional.finrank_eq_card_basis'
theorem FiniteDimensional.finrank_eq_card_basis' :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {ι : Type w}, Basis ι K V → ↑(FiniteDimensional.finrank K V) = Cardinal.mk ι
This theorem states that if we have a vector space that is finite-dimensional over a division ring, then the cardinality of any basis of this vector space is equal to its rank. Here, the rank (or `finrank`) of a vector space is defined as the natural number equivalent of the cardinality of a basis. In simpler terms, the theorem says that the number of basis vectors in a finite-dimensional vector space is equal to the dimension of the vector space. In mathematical notation, this would be represented as $\#(\text{basis}) = \text{dim}(V)$ where $V$ is the vector space.
More concisely: In a finite-dimensional vector space over a division ring, the number of basis vectors equals the dimension.
|
FiniteDimensional.eq_of_le_of_finrank_le
theorem FiniteDimensional.eq_of_le_of_finrank_le :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S₁ S₂ : Submodule K V} [inst_3 : FiniteDimensional K ↥S₂],
S₁ ≤ S₂ → FiniteDimensional.finrank K ↥S₂ ≤ FiniteDimensional.finrank K ↥S₁ → S₁ = S₂
The theorem `FiniteDimensional.eq_of_le_of_finrank_le` states that for any division ring `K` and any additive commutative group `V` that forms a module over `K`, given two submodules `S₁` and `S₂` of `V` such that `S₂` is finite-dimensional, if `S₁` is contained within `S₂` and the rank (or dimension) of `S₂` is less than or equal to the rank of `S₁`, then the two submodules `S₁` and `S₂` are equal. This means that in a finite-dimensional context, containment and having the same or smaller dimension are sufficient conditions for two submodules to be identical.
More concisely: If `S₁` is a submodule of the finite-dimensional module `V` over a division ring `K`, and `S₂` contains `S₁` with smaller or equal dimension, then `S₁ = S₂`.
|