Basis.finite_index_of_rank_lt_aleph0
theorem Basis.finite_index_of_rank_lt_aleph0 :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type u_1} {s : Set ι},
Basis (↑s) R M → Module.rank R M < Cardinal.aleph0 → s.Finite
This theorem states that if a module has a finite dimension, then all bases of the module are indexed by a finite set. In other words, for any ring `R`, a module `M` over the ring, and a set `s` indexing the basis of the module, if the module rank (equivalent to the dimension in the linear algebra context) is less than `ℵ₀` (the smallest infinite cardinal number), then the set `s` is finite. This implies that the number of basis elements (which forms a foundation for the module) is finite. The theorem holds under the assumption of a strong rank condition for the ring `R`, which is a certain property about the linear independence of sets in the module.
More concisely: If `M` is a finite-dimensional module over a ring `R` satisfying a strong rank condition, then `M` has a finite basis.
|
CompleteLattice.Independent.subtype_ne_bot_le_finrank
theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank :
∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] [inst_5 : NoZeroSMulDivisors R M]
{p : ι → Submodule R M},
CompleteLattice.Independent p →
∀ [inst_6 : Fintype { i // p i ≠ ⊥ }], Fintype.card { i // p i ≠ ⊥ } ≤ FiniteDimensional.finrank R M
The theorem `CompleteLattice.Independent.subtype_ne_bot_le_finrank` states that if we have a set `p` of independent submodules of a module `M` over a ring `R` that has finite rank, then the number of nontrivial (i.e., not zero) submodules in `p` is at most the rank of `M`. This means if `p` is a set where each element points to a submodule of `M` and we only count the elements where the corresponding submodule isn't the zero submodule (denoted as `⊥`), the number of those elements doesn't exceed the dimension of the module `M`. The prerequisite that `p` is independent means that no submodule within `p` can be represented as a combination of any other submodules within `p`. Note that the theorem requires a proof that the set of nontrivial elements in `p` is finite, which can be provided by `CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional`.
More concisely: If `M` is a finitely-generated module over a ring `R` and `p` is a finite set of independent submodules of `M`, then the number of non-zero submodules in `p` is at most the rank of `M`.
|
FiniteDimensional.finrank_eq_zero_iff_isTorsion
theorem FiniteDimensional.finrank_eq_zero_iff_isTorsion :
∀ {M : Type v} [inst : AddCommGroup M] {R : Type u_1} [inst_1 : CommRing R] [inst_2 : StrongRankCondition R]
[inst_3 : IsDomain R] [inst_4 : Module R M] [inst_5 : Module.Finite R M],
FiniteDimensional.finrank R M = 0 ↔ Module.IsTorsion R M
This theorem states that for a given module `M` over a commutative ring `R`, with `R` satisfying the `StrongRankCondition` and being a domain, and `M` being a finite module, the finite rank of `M` over `R` is zero if and only if `M` is a torsion module.
In other words, the theorem proves an equivalence between the module having no basis elements (having rank zero) and every element of the module becoming annihilated by multiplication with some non-zero element from the ring, which is the definition of a torsion module. This theorem is valid under the assumptions that the ring `R` is a domain and satisfies the `StrongRankCondition`, and the module `M` is finite. The `StrongRankCondition` implies that every linearly independent set in a module has cardinality less than or equal to the rank of the module.
More concisely: For a finite module M over a commutative domain R satisfying the StrongRankCondition, M has rank 0 if and only if every element in M is a torsion element.
|
Submodule.rank_eq_zero
theorem Submodule.rank_eq_zero :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : NoZeroSMulDivisors R M] {S : Submodule R M}, Module.rank R ↥S = 0 ↔ S = ⊥
This theorem states that for any ring `R`, additive commutative group `M`, and `M` being a module over `R`, with the condition that `R` is nontrivial and there are no zero scalar multiplication or division operations in `R` and `M`, the rank of a submodule `S` of `M` is equal to zero if and only if `S` is the zero submodule. This theorem is used to relate the algebraic property of a submodule (its rank) to its structural property (being the zero submodule).
More concisely: For any nontrivial ring `R`, module `M` over `R`, and submodule `S` of `M` with no zero scalar multiplication or division in `R` and `M`, the rank of `S` is zero if and only if `S` is the zero submodule.
|
LinearIndependent.cardinal_mk_le_finrank
theorem LinearIndependent.cardinal_mk_le_finrank :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] {ι : Type w} {b : ι → M},
LinearIndependent R b → Cardinal.mk ι ≤ ↑(FiniteDimensional.finrank R M)
This theorem states that for any Ring `R`, Additive Commutative Group `M`, where `M` is also a module over `R`, with `R` having the strong rank condition and `M` being a finite module, and any type `ι` with a function `b` from `ι` to `M` such that `b` defines a linearly independent set, the cardinality of type `ι` (i.e., the size of the set of linearly independent vectors) is less than or equal to the rank (i.e., the dimension) of the module `M` over `R`. In other words, the size of any linearly independent set in a vector space cannot exceed the dimension of that space.
More concisely: For any ring `R` with the strong rank condition, finite module `M` over `R`, and a linearly independent set `b : ι → M` from a type `ι`, the cardinality of `ι` is bounded by the rank of `M` as a module over `R`.
|
rank_eq_one
theorem rank_eq_one :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] [inst_4 : StrongRankCondition R] (v : M),
v ≠ 0 → (∀ (w : M), ∃ c, c • v = w) → Module.rank R M = 1
This theorem states that for any type `R` of ring, and any type `M` of module over `R` with the properties of being an additive commutative group, a module, having no zero scalar multiplication divisors, and having a strong rank condition, if there is a nonzero vector `v` in `M`, and every other vector in `M` can be expressed as a scalar multiple of `v`, then the rank of the module `M` is one. In simpler terms, if a module contains only multiples of a single, non-zero vector, it is one-dimensional.
More concisely: If `M` is a non-zero, finitely generated `R`-module satisfying the conditions of being an additive commutative group, having no zero scalar multiplication divisors, and having a strong rank condition, then the rank of `M` is 1 if and only if every element of `M` is a scalar multiple of some non-zero vector in `M`.
|
cardinal_mk_le_finrank_of_linearIndependent
theorem cardinal_mk_le_finrank_of_linearIndependent :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] {ι : Type w} {b : ι → M},
LinearIndependent R b → Cardinal.mk ι ≤ ↑(FiniteDimensional.finrank R M)
The theorem `cardinal_mk_le_finrank_of_linearIndependent` asserts the following: for any ring `R`, any additive commutative group `M` that also forms a module over `R`, any set `ι`, and any family of vectors `b : ι → M` which are linearly independent over `R`, the cardinality of the set `ι` (i.e., the number of vectors in the family `b`) is less than or equal to the (finite) rank of the module `M` over `R`. In other words, the number of linearly independent vectors in a module can never exceed the dimension of the module.
More concisely: The number of linearly independent vectors in a module over a ring is less than or equal to the finite rank of the module.
|
finrank_bot
theorem finrank_bot :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R],
FiniteDimensional.finrank R ↥⊥ = 0
This theorem states that for any ring `R` and any commutative additive group `M` that is also a module over `R`, provided that `R` is nontrivial, the rank of the bottom (`⊥`) submodule is `0`. In other words, the dimension of the trivial subspace in any vector space is zero.
More concisely: For any nontrivial ring `R` and commutative additive group `M` that is also an `R`-module, the rank of the zero submodule is 0.
|
rank_bot
theorem rank_bot :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R],
Module.rank R ↥⊥ = 0
This theorem, named `rank_bot`, states that for any ring `R`, type `M` equipped with the structure of an additive commutative group and an `R`-module, and assuming `R` is nontrivial (i.e., not all elements of `R` are the same), the rank of the trivial submodule (denoted `⊥`) is 0. In mathematical terms, if `M` is a module over a nontrivial ring `R`, then the dimension (rank) of the trivial submodule of `M` is zero.
More concisely: The rank of the trivial submodule of an `R`-module `M` over a nontrivial ring `R` is 0.
|
finrank_eq_zero_of_basis_imp_false
theorem finrank_eq_zero_of_basis_imp_false :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M], (∀ (s : Finset M), Basis (↑↑s) R M → False) → FiniteDimensional.finrank R M = 0
The theorem `finrank_eq_zero_of_basis_imp_false` states that for any type `R` serving as a Ring, and any type `M` forming an Additive Commutative Group and a Module over `R`, with `M` being a free module over `R`, if it is impossible for any finite set `s` of elements of `M` to form a basis for the module `M` over `R`, then the rank (as a natural number) of the module `M` over `R`, which is defined as `0` for infinite rank, must be `0`. In mathematical terms, if a vector space has no finite basis, it must be of dimension `0`.
More concisely: If a free module over a ring has no finite basis, then its rank is 0.
|
finset_card_le_finrank_of_linearIndependent
theorem finset_card_le_finrank_of_linearIndependent :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] {b : Finset M},
(LinearIndependent R fun x => ↑x) → b.card ≤ FiniteDimensional.finrank R M
This theorem, referred to as `finset_card_le_finrank_of_linearIndependent`, asserts that for any Ring `R`, an Additive Commutative Group `M` and a Module structure over `R` and `M`; given that `R` satisfies the strong rank condition and the module is finite. If we have a finite set `b` of `M` such that the function from `b` to `M` is a linearly independent family of vectors, then the cardinality of the finset `b` is less than or equal to the rank (as a natural number) of the module of `M` over `R`.
In other words, the number of linearly independent vectors in a set cannot exceed the rank of the module they belong to.
More concisely: For any ring R, additive commutative group M with a module structure over R, and a finite, linearly independent set b of vectors in M, the cardinality of b is less than or equal to the rank of M as a module over R.
|
rank_pos_iff_nontrivial
theorem rank_pos_iff_nontrivial :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : NoZeroSMulDivisors R M], 0 < Module.rank R M ↔ Nontrivial M
This theorem states that for a given ring `R` and an additive commutative group `M`, which is also a module over `R`, the rank of the module `M` is greater than 0 if and only if `M` is nontrivial, given that `R` is nontrivial and there are no zero scalar multiplicative divisors in `R` and `M`. In mathematical terms, it means that the dimension of a vector space (which is equivalent to the rank of a module in this context) is positive if and only if that vector space is nontrivial (i.e., it contains more than just the zero vector).
More concisely: The rank of a nontrivial additive commutative group `M` over a nontrivial ring `R` without zero scalar multiplicative divisors is positive.
|
finrank_le_one
theorem finrank_le_one :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] [inst_4 : StrongRankCondition R] (v : M),
(∀ (w : M), ∃ c, c • v = w) → FiniteDimensional.finrank R M ≤ 1
This theorem states that if every vector in a module `M` over a ring `R` can be expressed as a scalar multiple of a specific vector `v` (that is, `∀ (w : M), ∃ c, c • v = w`), then the rank (or finite dimension) of the module `M` is at most 1 (`FiniteDimensional.finrank R M ≤ 1`). Here, the ring `R` is assumed to have no zero divisors under scalar multiplication (`NoZeroSMulDivisors R M`) and to satisfy the Strong Rank Condition (`StrongRankCondition R`). In other words, if all vectors in `M` are scalar multiples of a single vector, `M` is one-dimensional or less.
More concisely: If a module M over a ring R with no zero divisors under scalar multiplication and satisfying the Strong Rank Condition has every vector expressible as a scalar multiple of a specific vector, then the rank of M is at most 1.
|
LinearIndependent.fintype_card_le_finrank
theorem LinearIndependent.fintype_card_le_finrank :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] {ι : Type u_1} [inst_5 : Fintype ι] {b : ι → M},
LinearIndependent R b → Fintype.card ι ≤ FiniteDimensional.finrank R M
This theorem states that for any ring `R`, additive commutative group `M`, and module `M` over `R` with the strong rank condition and finiteness, and any finite type `ι` with a function `b` mapping `ι` to `M` that is linearly independent over `R`, the cardinality of `ι` (i.e., the number of elements in `ι`) is less than or equal to the rank of the module `M` over `R`. In other words, the number of linearly independent vectors in a vector space (or module) cannot exceed the dimension of that space.
More concisely: For any ring `R`, additive commutative group `M` as an `R`-module with the strong rank condition and finiteness, any function `b` mapping a finite type `ι` to `M` that is linearly independent over `R`, the cardinality of `ι` is bounded above by the rank of `M` over `R`.
|
Module.Finite.lt_aleph0_of_linearIndependent
theorem Module.Finite.lt_aleph0_of_linearIndependent :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type w} [inst_4 : Module.Finite R M] {v : ι → M},
LinearIndependent R v → Cardinal.mk ι < Cardinal.aleph0
This theorem, named `Module.Finite.lt_aleph0_of_linearIndependent`, states that for any ring `R`, additive commutative group `M` and module `R M` satisfying the strong rank condition, if `v` is a linearly independent family of vectors over `R` in the finite module `M`, indexed by a type `ι`, then the cardinality of the type `ι` is strictly less than the smallest infinite cardinal (also known as `aleph-zero` or `ℵ₀`). In mathematical terms, this is saying that if a vector space has a finite dimension, then any set of linearly independent vectors in that vector space must be finite.
More concisely: If `R` is a ring, `M` is an additive commutative `R`-module satisfying the strong rank condition, and `v` is a linearly independent family of vectors in the finite `R`-module `M` indexed by a type `ι`, then `card ι < ℵ₀`.
|
FiniteDimensional.finrank_pos_iff
theorem FiniteDimensional.finrank_pos_iff :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : StrongRankCondition R] [inst_5 : Module.Finite R M] [inst_6 : NoZeroSMulDivisors R M],
0 < FiniteDimensional.finrank R M ↔ Nontrivial M
This theorem states that for a module `M` over a ring `R`, which is both torsion-free and finite (`Module.Finite R M`), and meets the conditions of being non-trivial (`Nontrivial R`) and satisfying the strong rank condition (`StrongRankCondition R`), it has a positive rank (`0 < FiniteDimensional.finrank R M`) if and only if the module `M` itself is non-trivial (`Nontrivial M`). Here, 'non-trivial' refers to the property that the module contains an element that is not the zero element, and 'torsion-free' means that there is no non-zero scalar in `R` that multiplies a non-zero element of `M` to give the zero element in `M`.
More concisely: A finite, torsion-free module over a ring with the strong rank condition is non-trivial if and only if it has positive rank.
|
FiniteDimensional.finrank_pos
theorem FiniteDimensional.finrank_pos :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : StrongRankCondition R] [inst_5 : Module.Finite R M] [inst_6 : NoZeroSMulDivisors R M]
[h : Nontrivial M], 0 < FiniteDimensional.finrank R M
This theorem states that for any nontrivial finite dimensional space, its associated `finrank` (the rank of a module as a natural number) is positive. More formally, given a ring `R`, a module `M` over `R`, and under the conditions that `R` is nontrivial, `R` has the strong rank condition, `M` is a finite module over `R`, there are no zero scalar multipliers and divisors in `M`, and `M` itself is nontrivial, then the `finrank` of `M` over `R` is strictly greater than zero.
More concisely: if R is a nontrivial ring satisfying the strong rank condition, and M is a finite, nontrivial module over R with no zero scalar multipliers or divisors, then the rank of M is positive.
|
FiniteDimensional.nontrivial_of_finrank_pos
theorem FiniteDimensional.nontrivial_of_finrank_pos :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : NoZeroSMulDivisors R M], 0 < FiniteDimensional.finrank R M → Nontrivial M
The theorem `FiniteDimensional.nontrivial_of_finrank_pos` asserts that for any ring `R`, any additive commutative group `M`, and any module `M` over the ring `R`, if `M` is a finite-dimensional space with positive rank (as per the `FiniteDimensional.finrank` function), and the ring `R` is nontrivial (contains at least one non-zero element), and there are no zero scalar multipliers or divisors for `R` and `M`, then `M` is also nontrivial (contains at least one non-zero element).
More concisely: If a finite-dimensional module over a nontrivial ring has positive rank and has no zero scalar multipliers or divisors, then it contains a non-zero element.
|
FiniteDimensional.finrank_zero_iff
theorem FiniteDimensional.finrank_zero_iff :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : StrongRankCondition R] [inst_5 : Module.Finite R M] [inst_6 : NoZeroSMulDivisors R M],
FiniteDimensional.finrank R M = 0 ↔ Subsingleton M
This theorem states that a finite-dimensional space over a ring `R` has a rank of zero if and only if it is a subsingleton. Here, a subsingleton is a set or type with at most one element. This theorem is the `finrank` version of `rank_zero_iff`, meaning it concerns the rank defined in the context of finite-dimensional spaces.
The theorem applies to a module `M` over a ring `R`, assuming that `R` is nontrivial (i.e., not a zero ring), satisfies the strong rank condition (which implies that submodules of free modules are free), has finite rank, and has no zero `s`-multiples or divisors. All these conditions are encapsulated in the assumptions `[inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R] [inst_4 : StrongRankCondition R] [inst_5 : Module.Finite R M] [inst_6 : NoZeroSMulDivisors R M]`.
More concisely: A finite-dimensional module over a nontrivial ring with the strong rank condition, finite rank, and no zero multiples or divisors has rank zero if and only if it is a subsingleton.
|
rank_zero_iff
theorem rank_zero_iff :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : NoZeroSMulDivisors R M], Module.rank R M = 0 ↔ Subsingleton M
This theorem states that for any ring `R` and additively commutative group `M` which forms a `R`-module `M` (with `R` being nontrivial and no nonzero scalar multiplication divisors between `R` and `M`), the rank of the `R`-module `M` is zero if and only if `M` is a subsingleton. In other words, a module `M` over a ring `R` has a rank of zero precisely when `M` is a subsingleton, provided `R` doesn't have any trivial elements and no nonzero elements of `R` annihilate `M` when used as scalar multipliers.
More concisely: For an additively commutative group `M` being an `R`-module over a nontrivial ring `R` without nonzero scalar multiplication divisors, the rank of `M` is zero if and only if `M` is a subsingleton.
|
Basis.nonempty_fintype_index_of_rank_lt_aleph0
theorem Basis.nonempty_fintype_index_of_rank_lt_aleph0 :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type u_1},
Basis ι R M → Module.rank R M < Cardinal.aleph0 → Nonempty (Fintype ι)
This theorem states that if a module, denoted as `M`, over a ring, denoted as `R`, has a finite dimension (specifically, its rank is less than `aleph0`, the smallest infinite cardinal number), then for any basis of `M`, denoted by `ι`, there exists a finite type that can index this basis. In other words, all bases of a finite-dimensional module are indexed by a finite type. The `StrongRankCondition` for `R` is assumed, which is a condition on the ring that ensures the uniqueness of rank for finitely generated free modules.
More concisely: If `M` is a finite-dimensional module over the ring `R` with StrongRankCondition, then `M` has a basis indexed by a finite type.
|
Module.exists_nontrivial_relation_of_finrank_lt_card
theorem Module.exists_nontrivial_relation_of_finrank_lt_card :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] {t : Finset M},
FiniteDimensional.finrank R M < t.card → ∃ f, (t.sum fun e => f e • e) = 0 ∧ ∃ x ∈ t, f x ≠ 0
This theorem states that for any given type `R` which is a ring, type `M` which is an additively commutative group and a module over `R`, given the `StrongRankCondition` for `R` and `M` being a finite `Module` over `R`, if there exists a finite set `t` of elements of `M` such that the cardinality of `t` is greater than the rank of the module `M` over the ring `R` (also known as the dimension of `M` as a vector space over `R`), then there exists a nontrivial linear relation among the elements of `t`. In other words, there exists a function `f` such that the sum of `f(e) * e` for all `e` in `t` is zero and there is an element `x` in `t` for which `f(x)` is not zero. This theorem is a version of the well-known fact from linear algebra that in any vector space, if you have more vectors than the dimension of the space, then they must be linearly dependent.
More concisely: Given a ring `R`, an additively commutative group and `R`-module `M` with finite rank, if `M` has a finite generating set `t` larger than its rank, then there exist non-zero scalars `f(e)` for each `e` in `t` such that the sum of `f(e) * e` is zero.
|
fintype_card_le_finrank_of_linearIndependent
theorem fintype_card_le_finrank_of_linearIndependent :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] {ι : Type u_1} [inst_5 : Fintype ι] {b : ι → M},
LinearIndependent R b → Fintype.card ι ≤ FiniteDimensional.finrank R M
This theorem, `fintype_card_le_finrank_of_linearIndependent`, states that for any ring `R`, and any additive commutative group `M` that forms a module `M` over the ring `R`, under the condition of strong rank condition and the module `M` being finite, for any type `ι` that has finite number of elements, and any function `b` from `ι` to `M`, if the set of vectors `b` are linearly independent, then the number of elements in `ι` (`Fintype.card ι`) is less than or equal to the rank of the module `M` over the ring `R` (`FiniteDimensional.finrank R M`). In other words, the cardinality of a finite set of linearly independent vectors in a finite-dimensional module cannot exceed the dimension of the module.
More concisely: For any ring R, additive commutative group M forming an R-module, under the strong rank condition and M being finite, if ι has finitely many elements and the vectors in the function b from ι to M are linearly independent, then Fintype.card ι ≤ FiniteDimensional.finrank R M.
|
rank_eq_zero_iff
theorem rank_eq_zero_iff :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Module.rank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
This theorem, `rank_eq_zero_iff`, states that for any ring `R` and additive commutative group `M` that forms a module `M` over `R`, the rank of this module `M` is zero if and only if for every element `x` in `M`, there is a nonzero scalar `a` from `R` such that the scalar multiplication of `a` and `x` equals zero. The theorem provides a characterization for a module having zero rank in terms of its elements being annihilated by a nonzero scalar from the ring.
More concisely: A module over a ring has rank zero if and only if every element in the module is annihilated by some nonzero scalar in the ring.
|
FiniteDimensional.finrank_eq_zero_iff
theorem FiniteDimensional.finrank_eq_zero_iff :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M],
FiniteDimensional.finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
This theorem states that for any ring `R`, an additive commutative group `M`, and a module structure over `R` and `M` satisfying the strong rank condition and being finite, the rank of the module (as defined by `FiniteDimensional.finrank`) is equal to zero if and only if for every element `x` in `M`, there exists a non-zero element `a` such that scaling `x` by `a` yields the zero element. In other words, the module has rank zero precisely when every element of the module can be annihilated by some non-zero scalar from the ring.
More concisely: A finite, commutative `R`-module `M` has rank zero if and only if for every `x` in `M`, there exists a non-zero `a` in `R` such that `ax = 0`.
|
LinearIndependent.lt_aleph0_of_finite
theorem LinearIndependent.lt_aleph0_of_finite :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type w} [inst_4 : Module.Finite R M] {v : ι → M},
LinearIndependent R v → Cardinal.mk ι < Cardinal.aleph0
The theorem `LinearIndependent.lt_aleph0_of_finite` states the following: Let `R` be a ring, `M` be an additive commutative group which is also an `R`-module. Suppose that `R` satisfies the strong rank condition, and `M` is a finite `R`-module. Now consider a family of vectors `v` indexed over the type `ι`. If this family of vectors is linearly independent over `R`, then the cardinal number of the type `ι` (i.e., the "size" of the index set) is strictly less than `ℵ₀`, the smallest infinite cardinal number. This essentially means that the family `v` cannot have 'infinitely many' vectors if it is to remain linearly independent in this context.
More concisely: A finite linearly independent family of vectors over a ring `R` in an `R`-module `M` satisfies the size of its index set being strictly less than the first infinite cardinal number `ℵ₀`.
|
Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card
theorem Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] {t : Finset M},
FiniteDimensional.finrank R M + 1 < t.card →
∃ f, (t.sum fun e => f e • e) = 0 ∧ (t.sum fun e => f e) = 0 ∧ ∃ x ∈ t, f x ≠ 0
This theorem states that if a finite set (`Finset`) of elements from a module `M` over a ring `R` has a cardinality greater than the rank (finite dimension) of `M` plus one, then there exists a nontrivial linear relation among the elements of the set such that the coefficients of the relation add up to zero. This linear relation is represented by a function `f` that assigns to each element of the set a coefficient, and the conditions on `f` are that the sum of the scaled elements is zero and the sum of the coefficients is zero. Additionally, there is at least one element in the set for which the corresponding coefficient is not zero, making the relation nontrivial. The theorem assumes that the ring `R` satisfies the strong rank condition and that the module `M` is finite.
More concisely: If `M` is a finite module over a ring `R` satisfying the strong rank condition, then any finite subset of `M` with cardinality greater than the rank of `M` + 1 contains linearly dependent elements.
|
FiniteDimensional.finrank_zero_of_subsingleton
theorem FiniteDimensional.finrank_zero_of_subsingleton :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : Subsingleton M], FiniteDimensional.finrank R M = 0
The theorem `FiniteDimensional.finrank_zero_of_subsingleton` states that for any type R of ring, type M of additive commutative group, where M is a module over R, and if R is nontrivial and M is a subsingleton (has at most one element), then the finite rank of M over R is zero. In other words, a finite-dimensional module that has at most one element has zero rank.
More concisely: If R is a nontrivial ring and M is a subsingleton module over R, then the rank of M as an R-module is zero.
|
FiniteDimensional.finrank_pos_iff_exists_ne_zero
theorem FiniteDimensional.finrank_pos_iff_exists_ne_zero :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : StrongRankCondition R] [inst_5 : Module.Finite R M] [inst_6 : NoZeroSMulDivisors R M],
0 < FiniteDimensional.finrank R M ↔ ∃ x, x ≠ 0
The theorem `FiniteDimensional.finrank_pos_iff_exists_ne_zero` states that for any ring `R`, any Additive Commutative Group `M`, any `R`-module `M`, and given that `R` is nontrivial, `R` satisfies the strong rank condition, `M` is a finite `R`-module, and there are no zero scalar multiplication divisors in `R` and `M`, the rank (dimension) of the module `M` over the ring `R` is greater than zero if and only if there exists a nonzero element in `M`. In other words, in the context of modules over a ring, this theorem connects the non-zeroness of an element in a module with the positivity of the module's rank.
More concisely: For an nontrivial ring `R` satisfying the strong rank condition, a finite `R`-module `M` has positive rank if and only if there exists a nonzero element in `M`.
|
finrank_eq_one
theorem finrank_eq_one :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] [inst_4 : StrongRankCondition R] (v : M),
v ≠ 0 → (∀ (w : M), ∃ c, c • v = w) → FiniteDimensional.finrank R M = 1
The theorem `finrank_eq_one` states that for any ring `R` and any module `M` over `R`, if there exists a non-zero vector in `M` such that every other vector in `M` can be expressed as a scalar multiple of it, then the module `M` has a dimension of one. This theorem also requires the ring `R` to be a no-zero-divisor and have a strong rank condition. In mathematical terms, it could be said that this theorem describes a one-dimensional vector space or module, where all vectors are scalar multiples of a given non-zero vector.
More concisely: If a module over a no-zero-divisor ring has a linearly dependent non-zero basis, then its dimension is equal to 1.
|
rank_subsingleton'
theorem rank_subsingleton' :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : Subsingleton M], Module.rank R M = 0
The theorem `rank_subsingleton'` states that for any type `R` that has a ring structure and any type `M` that is an additive commutative group and a module over `R`, if `R` is nontrivial (meaning it contains at least two distinct elements) and `M` is a subsingleton (meaning it contains at most one distinct element), then the rank of the module `M` over the ring `R` is zero.
More concisely: If `R` is a nontrivial ring and `M` is a subsingleton additive commutative group that is an `R`-module, then the rank of `M` over `R` is 0.
|
FiniteDimensional.nontrivial_of_finrank_eq_succ
theorem FiniteDimensional.nontrivial_of_finrank_eq_succ :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
[inst_4 : NoZeroSMulDivisors R M] {n : ℕ}, FiniteDimensional.finrank R M = n.succ → Nontrivial M
This theorem states that if the rank of a finite-dimensional space (denoted by `FiniteDimensional.finrank R M`) is the successor of a natural number `n` (i.e., `n.succ`), then this space is nontrivial. Here, a space is considered nontrivial if it contains at least one non-zero element. The space is defined over a ring `R` and the module `M` is an additive commutative group that also forms a module over `R`. The conditions `Nontrivial R` and `NoZeroSMulDivisors R M` ensure that the ring `R` is nontrivial and that the scalar multiplication and division in the module `M` do not yield zero unless multiplied or divided by zero.
More concisely: If a finite-dimensional space over a nontrivial ring has rank strictly greater than a natural number, then it contains a non-zero element.
|