rank_eq_card_basis
theorem rank_eq_card_basis :
∀ {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 : Fintype ι],
Basis ι R M → Module.rank R M = ↑(Fintype.card ι)
This theorem states that for any Ring `R`, Additive Commutative Group `M`, and a Module structure over `R` and `M` satisfying the Strong Rank Condition, and for any index type `ι` which is finite (that is, it has a `Fintype` instance), if there exists a Basis indexed by `ι` for the Module, then the rank of the Module (which is a cardinal number) is equal to the number of elements in `ι` (the cardinality of the basis).
More concisely: For any ring `R`, additive commutative group `M` with a Module structure over `R`, satisfying the Strong Rank Condition, with a finite index type `ι` having a Basis for the Module, the rank of the Module equals the cardinality of `ι`.
|
Basis.card_le_card_of_linearIndependent
theorem Basis.card_le_card_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 u_1} [inst_4 : Fintype ι],
Basis ι R M →
∀ {ι' : Type u_2} [inst_5 : Fintype ι'] {v : ι' → M},
LinearIndependent R v → Fintype.card ι' ≤ Fintype.card ι
This theorem states that for any ring `R`, additive commutative group `M`, and `M` is a module over `R` with the strong rank condition, given a basis `ι` for `M` over `R` and a linearly independent family of vectors `v` in `M` indexed by `ι'`, if `ι'` and `ι` are both finite types, then the number of elements in `ι'` is less than or equal to the number of elements in `ι`. In simpler terms, in a vector space with a strong rank condition, the size of any linearly independent set cannot exceed the size of any basis of the vector space.
More concisely: In a module over a ring with the strong rank condition, the size of any linearly independent family is less than or equal to the size of any basis.
|
FiniteDimensional.finrank_eq_rank
theorem FiniteDimensional.finrank_eq_rank :
∀ (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) = Module.rank R M
This theorem, titled `FiniteDimensional.finrank_eq_rank`, establishes that for a given module `M` over a ring `R`, if `M` is finite, then the rank of `M` is equal to its finite rank. Specifically, it states that for any `R` and `M` where `R` is a ring, `M` is an additive commutative group, `M` is a module over `R`, `R` satisfies the strong rank condition, and `M` is a finite module, the cardinality of the finite rank of `M` is equal to the rank of the module `M` over `R`. The strong rank condition is a property of rings that ensures the rank of a free module over the ring is well-defined.
More concisely: For a finite module M over a ring R satisfying the strong rank condition, the rank of M equals its finite rank.
|
linearIndependent_le_span'
theorem linearIndependent_le_span' :
∀ {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} (v : ι → M),
LinearIndependent R v →
∀ (w : Set M) [inst_4 : Fintype ↑w], Set.range v ≤ ↑(Submodule.span R w) → Cardinal.mk ι ≤ ↑(Fintype.card ↑w)
This theorem states that if a ring `R` satisfies the strong rank condition, then for any family of vectors `v : ι → M` that are linearly independent over `R` and are contained within the span of a finite set `w : Set M`, the cardinality (or size) of `ι` is less than or equal to the cardinality of `w`. In other words, the number of linearly independent vectors in the span of a finite set in a module over a ring with the strong rank condition can't exceed the number of vectors in the underlying set.
More concisely: In a ring satisfying the strong rank condition, the number of linearly independent vectors in a module over it from a finite set is less than or equal to the number of vectors in that set.
|
linearIndependent_le_span_finset
theorem linearIndependent_le_span_finset :
∀ {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} (v : ι → M),
LinearIndependent R v → ∀ (w : Finset M), Submodule.span R ↑w = ⊤ → Cardinal.mk ι ≤ ↑w.card
This theorem states that given a type `R` of a ring, a type `M` of an additive commutative group, a module `M` over `R`, a strong rank condition over `R`, and a function `v` from a type `ι` to `M`, if `v` is linearly independent over `R`, then for any finite set `w` of elements in `M`, if the span of `w` is equal to the top element (representing the whole space), then the cardinality of `ι` is less than or equal to the number of elements in `w`. In other words, it implies that the size of any linearly independent set in a finite-dimensional space cannot be larger than the dimension of the space itself.
More concisely: Given a ring `R`, an additive commutative group `M` with a finite-dimensional module structure over `R`, a strong rank condition, and a linearly independent set `v` from a type `ι` in `M`, the cardinality of `ι` is bounded above by the number of elements in any finite spanning set of `M`.
|
linearIndependent_le_infinite_basis
theorem linearIndependent_le_infinite_basis :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type w},
Basis ι R M →
∀ [inst_4 : Infinite ι] {κ : Type w} (v : κ → M), LinearIndependent R v → Cardinal.mk κ ≤ Cardinal.mk ι
This theorem, named `linearIndependent_le_infinite_basis`, states that for any ring `R`, additive commutative group `M`, and module `M` over `R` with the strong rank condition, given any basis `b` indexed by a type `ι`, if `ι` is infinite and there is a family of vectors `v` indexed by a type `κ` that are linearly independent over `R`, then the cardinality of `κ` is less than or equal to the cardinality of `ι`. In other words, in a vector space over a ring with strong rank condition, the cardinality of any set of linearly independent vectors is not greater than the cardinality of an infinite basis.
More concisely: In a vector space over a commutative ring with the strong rank condition, the size of any linearly independent set is less than or equal to the size of an infinite basis.
|
FiniteDimensional.finrank_eq_card_finset_basis
theorem FiniteDimensional.finrank_eq_card_finset_basis :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type w} {b : Finset ι},
Basis { x // x ∈ b } R M → FiniteDimensional.finrank R M = b.card
The theorem `FiniteDimensional.finrank_eq_card_finset_basis` states that for any ring `R`, any additive commutative group `M`, and any module structure over `M` with respect to `R` having a strong rank condition, if we have a basis `b` of `M` represented as a finite set (a `Finset`) and indexed by some type `ι`, then the rank or dimension of the module `M` (which is defined to be `0` if the module has infinite rank or dimension) is equal to the cardinality of the basis `b`. In other words, the dimension of a finite-dimensional vector space or module is reflected by the number of elements in its basis.
More concisely: For any commutative ring R, additive group M with an R-module structure having a strong rank condition, the dimension of the finite-dimensional module M equals the cardinality of any basis represented as a finite set.
|
LinearIndependent.finite_of_le_span_finite
theorem LinearIndependent.finite_of_le_span_finite :
∀ {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} (v : ι → M),
LinearIndependent R v → ∀ (w : Set M) [inst_4 : Finite ↑w], Set.range v ≤ ↑(Submodule.span R w) → Finite ι
The theorem `LinearIndependent.finite_of_le_span_finite` states that, given a ring `R` that satisfies the strong rank condition, and a module `M` over `R`, any family of vectors `v : ι → M` that is linearly independent and is contained within the span of some finite set `w : Set M`, must itself be finite. In other words, if a set of vectors `v` is linearly independent and all its vectors can be expressed as linear combinations of a finite set `w`, then the set `v` must have a finite number of vectors.
More concisely: If `R` is a ring satisfying the strong rank condition and `M` is an `R`-module, any linearly independent family `v` of vectors in `M` contained within the span of a finite set `w` must itself be finite.
|
Basis.mk_eq_rank
theorem Basis.mk_eq_rank :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type w}
[inst_3 : StrongRankCondition R],
Basis ι R M → Cardinal.lift.{v, w} (Cardinal.mk ι) = Cardinal.lift.{w, v} (Module.rank R M)
This theorem states that for any ring `R`, additive commutative group `M`, and a `Module` structure over `R` and `M`, given a basis indexed by a type `ι` and assuming that `R` satisfies the strong rank condition, then the cardinality of the index set `ι` lifted to the maximum of its own universe and the universe of `M` is equal to the rank of the module `M` over `R` lifted to the maximum of its own universe and the universe of `ι`. In simpler terms, this theorem bridges the cardinality of the basis of a module and the rank of the module, under strong rank conditions.
More concisely: Given a ring `R`, an additive commutative group `M` with a `Module` structure over `R`, a basis `β: ι -> M`, and `R` satisfying the strong rank condition, the cardinality of `ι` equals the rank of `M` over `R`.
|
mk_eq_mk_of_basis
theorem mk_eq_mk_of_basis :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type w}
{ι' : Type w'} [inst_3 : InvariantBasisNumber R],
Basis ι R M → Basis ι' R M → Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')
The theorem `mk_eq_mk_of_basis` states that for any ring `R`, any additive commutative group `M` that is also a module over `R`, and any two types `ι` and `ι'` serving as the index sets for bases of the module, if the ring `R` satisfies the invariant basis number property (which says that every basis for a given vector space over a ring has the same cardinality), then the cardinality of the index set `ι`, when lifted to the maximum of the universes of `ι` and `ι'`, is equal to the cardinality of the index set `ι'`, when lifted to the maximum of the universes of `ι'` and `ι`. In simpler terms, if two sets serve as bases for a vector space, they must have the same cardinality.
More concisely: For any additive commutative group M being an R-module over a ring R satisfying the invariant basis number property, the cardinalities of any two index sets for its bases are equal when lifted to the maximum universe.
|
rank_self
theorem rank_self : ∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R], Module.rank R R = 1
This theorem, `rank_self`, states that for any type `R` which satisfies the conditions of being a ring (`Ring R`) and having a strong rank condition (`StrongRankCondition R`), the rank of the module over itself (`Module.rank R R`) is equal to 1. In mathematical terms, it's asserting that the rank of a ring as a module over itself is always 1, given that the ring satisfies the strong rank condition.
More concisely: For any ring `R` satisfying the strong rank condition, the rank of the `R`-module `R` is equal to 1.
|
Module.mk_finrank_eq_card_basis
theorem Module.mk_finrank_eq_card_basis :
∀ {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},
Basis ι R M → ↑(FiniteDimensional.finrank R M) = Cardinal.mk ι
This theorem states that for a given free module `M` over a ring `R` that has finite rank, any basis of this module labeled by the type `ι` will have a cardinality equal to the rank of the module. In other words, the cardinality of the set of basis elements is the same as the finite rank of the module. Here, StrongRankCondition is a condition about the rank of free modules, and Module.Finite indicates that `M` is a finite module.
More concisely: For a free module of finite rank over a ring, the number of elements in any basis is equal to the rank of the module.
|
finrank_eq_rank
theorem finrank_eq_rank :
∀ (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) = Module.rank R M
The theorem `finrank_eq_rank` states that for any ring `R` and any module `M` over `R`, if `M` satisfies the strong rank condition (a certain condition about the rank of submodules) and `M` is finite, then the finite rank of `M` is equal to the rank of `M`. Here, the rank and finite rank of a module are concepts related to its dimension; the rank refers to the size of a maximal linearly independent subset of `M`, while the finite rank is a variant that is defined to be zero for modules of infinite rank.
More concisely: For any ring `R` and finite module `M` over `R` satisfying the strong rank condition, the rank of `M` equals its finite rank.
|
Ideal.rank_eq
theorem Ideal.rank_eq :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : StrongRankCondition R] [inst_2 : Ring S]
[inst_3 : IsDomain S] [inst_4 : Algebra R S] {n : Type u_3} {m : Type u_4} [inst_5 : Fintype n]
[inst_6 : Fintype m], Basis n R S → ∀ {I : Ideal S}, I ≠ ⊥ → Basis m R ↥I → Fintype.card m = Fintype.card n
The theorem `Ideal.rank_eq` asserts that for any commutative ring `R` with a strong rank condition and a ring `S` which is an `R`-algebra and a domain, if `S` is a module-finite free `R`-algebra, then the `R`-rank of any non-zero `R`-free ideal `I` in `S` is equal to the rank of `S`. The `R`-rank here is defined in terms of the cardinality of the basis of the algebra or the ideal as a module over `R`. The conditions of `S` being a module-finite and free `R`-algebra, and `I` being a non-zero `R`-free ideal, are expressed in terms of the existence of bases for `S` and `I` respectively (as `R`-modules), which are indexed by finite types `n` and `m`. The theorem concludes that in these circumstances, the cardinalities of the types `n` and `m` - and hence the `R`-ranks of `S` and `I` - are equal.
More concisely: For a commutative ring `R` with a strong rank condition, an `R`-algebra `S` that is a module-finite free `R`-module of finite rank `n`, and a non-zero `R`-free ideal `I` in `S` of finite rank `m`, the ranks `n` and `m` are equal.
|
Basis.card_le_card_of_linearIndependent_aux
theorem Basis.card_le_card_of_linearIndependent_aux :
∀ {R : Type u_1} [inst : Ring R] [inst_1 : StrongRankCondition R] (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R),
LinearIndependent R v → m ≤ n
The theorem `Basis.card_le_card_of_linearIndependent_aux` states that for a Ring `R` satisfying the strong rank condition, if `m` elements of a free rank `n` `R`-module are linearly independent, then `m` must be less than or equal to `n`. In other words, the number of linearly independent vectors in a free module cannot exceed the rank of the module, given that the ring over which the module is defined possesses the strong rank condition.
More concisely: If a free module of rank n over a ring satisfying the strong rank condition has m linearly independent elements, then m ≤ n.
|
linearIndependent_le_basis
theorem linearIndependent_le_basis :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type w},
Basis ι R M → ∀ {κ : Type w} (v : κ → M), LinearIndependent R v → Cardinal.mk κ ≤ Cardinal.mk ι
The theorem `linearIndependent_le_basis` states that for any ring `R` satisfying the strong rank condition, if `b` is a basis for a module `M`, and `s` is a set of linearly independent vectors, then the cardinality (number of elements in the set) of `s` is less than or equal to the cardinality of `b`. This means that the size of any linearly independent set is bounded by the size of the basis in a module over a ring with the strong rank condition.
More concisely: For any module M over a ring R satisfying the strong rank condition, the number of linearly independent vectors in M is less than or equal to the number of vectors in any basis for M.
|
linearIndependent_le_span
theorem linearIndependent_le_span :
∀ {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} (v : ι → M),
LinearIndependent R v →
∀ (w : Set M) [inst_4 : Fintype ↑w], Submodule.span R w = ⊤ → Cardinal.mk ι ≤ ↑(Fintype.card ↑w)
This theorem states that if a ring `R` satisfies the strong rank condition, then for any family of vectors `v : ι → M` that is linearly independent over `R` and any finite set `w : Set M` that spans the module `M`, the cardinality of the index set `ι` is bounded by the cardinality of the set `w`. In other words, the number of linearly independent vectors cannot exceed the number of vectors in any finite spanning set.
More concisely: If a ring satisfies the strong rank condition, then the number of linearly independent vectors in any module is bounded by the number of vectors in any finite spanning set.
|
FiniteDimensional.finrank_eq_card_basis
theorem FiniteDimensional.finrank_eq_card_basis :
∀ {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 : Fintype ι],
Basis ι R M → FiniteDimensional.finrank R M = Fintype.card ι
The theorem `FiniteDimensional.finrank_eq_card_basis` states that for any ring `R`, any additive commutative group `M`, and any type `ι` with a finite number of elements, if `M` is a module over `R` and there exists a basis of `M` indexed by `ι`, then the rank (also known as the dimension) of the module `M` is equal to the number of elements in `ι`. In other words, the dimension of a vector space (or the rank of a module) over a ring is equal to the number of elements in a finite basis of the vector space (or module). The `StrongRankCondition R` assumption assures that the rank of any free module over `R` is well-defined.
More concisely: For any ring `R`, additive commutative group `M`, and finite type `ι`, if `M` is a free `R`-module with a basis of size `|ι|`, then the rank of `M` equals `|ι|`.
|
FiniteDimensional.finrank_self
theorem FiniteDimensional.finrank_self :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R], FiniteDimensional.finrank R R = 1
This theorem states that for any ring `R` that satisfies the `StrongRankCondition` (for instance, a `DivisionRing`), the rank of `R` as a module over itself is one. In other words, in the context of module theory, `R` is one-dimensional when considered over itself. This is measured using the function `FiniteDimensional.finrank`, which returns the rank of a module as a natural number. If the module has infinite rank, by convention, this function returns `0`. This theorem thus asserts a notable property of rings satisfying the `StrongRankCondition`: they are essentially as simple as possible from the perspective of their module-theoretic structure over themselves.
More concisely: For any ring `R` satisfying the `StrongRankCondition`, the rank of `R` as a module over itself, as measured by `FiniteDimensional.finrank`, is 1.
|
basis_le_span'
theorem basis_le_span' :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : RankCondition R] {ι : Type u_1},
Basis ι R M → ∀ {w : Set M} [inst_4 : Fintype ↑w], Submodule.span R w = ⊤ → Cardinal.mk ι ≤ ↑(Fintype.card ↑w)
This theorem, `basis_le_span'`, states that for any Ring `R`, Additive Commutative Group `M`, and a `Module` structure on `R` and `M`, if we have a `RankCondition` on `R` and a basis `ι` of `M`, then for any finite spanning set `w` of `M` such that the span of `w` is the whole module, the cardinality of the basis `ι` is less than or equal to the cardinality of the spanning set `w`. In mathematical terms, it asserts that for a module over a ring with a rank condition, any basis has cardinality less than or equal to that of any finite spanning set.
More concisely: For any module M over a ring with a rank condition, the size of a basis is less than or equal to the size of any finite spanning set.
|
Basis.mk_eq_rank''
theorem Basis.mk_eq_rank'' :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type v}, Basis ι R M → Cardinal.mk ι = Module.rank R M
This theorem states that for any ring `R`, any additive commutative group `M`, and any module `M` over the ring `R`, given the strong rank condition for `R`, and for any type `ι` which forms a basis of the module `M`, the cardinality of the basis type `ι` (denoted by `Cardinal.mk ι`) is equal to the rank of the module `M` over the ring `R` (denoted by `Module.rank R M`). Essentially, it is saying that the number of elements in a basis of a module (its cardinality) is equal to the rank of the module. This is a generalization of the familiar concept from linear algebra, where the rank of a vector space is the number of vectors in any basis.
More concisely: For any ring `R`, additive commutative group `M` as an `R`-module, and type `ι` forming a basis of `M`, the cardinality of `ι` equals the rank of `M` over `R`.
|
maximal_linearIndependent_eq_infinite_basis
theorem maximal_linearIndependent_eq_infinite_basis :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] {ι : Type w},
Basis ι R M →
∀ [inst_4 : Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v),
i.Maximal → Cardinal.mk κ = Cardinal.mk ι
The theorem states that for any ring `R` that satisfies the strong rank condition, if `b` is an infinite basis for a module `M`, then every maximal linearly independent set has the same cardinality as `b`. In other words, if you have a ring `R` with a module `M` that has a basis `b` which is infinite, any maximal set of vectors in `M` that are linearly independent (no vector in the set can be represented as a linear combination of the others) will have the same size (cardinality) as the basis `b`. This result is sourced from a paper by Lazarus (1973).
More concisely: In a ring satisfying the strong rank condition, every maximal linearly independent set of an infinite-dimensional module has the same cardinality as any infinite basis.
|
Basis.le_span''
theorem Basis.le_span'' :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : RankCondition R] {ι : Type u_1} [inst_4 : Fintype ι],
Basis ι R M → ∀ {w : Set M} [inst_5 : Fintype ↑w], Submodule.span R w = ⊤ → Fintype.card ι ≤ Fintype.card ↑w
The theorem `Basis.le_span''` states that for any ring `R` satisfying the rank condition and any additive commutative group `M` that is a module over `R`, given any finite basis `b : Basis ι R M` where `ι` is a finite type, and any finite spanning set `w : Set M`, if the span of `w` is the entire module (i.e., `Submodule.span R w = ⊤`), then the cardinality of `ι` (the size of the basis) is less than or equal to the cardinality of `w` (the size of the spanning set). In other words, in a module satisfying the rank condition, any finite basis has at most as many elements as any finite spanning set.
More concisely: In a module over a ring satisfying the rank condition, the size of a finite basis is less than or equal to the size of any finite spanning set.
|
FiniteDimensional.rank_lt_aleph0
theorem FiniteDimensional.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] [inst_4 : Module.Finite R M], Module.rank R M < Cardinal.aleph0
This theorem, known as `FiniteDimensional.rank_lt_aleph0` or an alias of `rank_lt_aleph0`, states that for any types `R` and `M`, where `R` is a ring, `M` is an additive commutative group, `R` satisfies the strong rank condition, and `M` is a finite `R`-module, the rank of the module `M` is less than `ℵ₀`, the smallest infinite cardinal. Essentially, this theorem asserts that the rank of a finite module is always finite.
More concisely: The rank of a finite commutative `R`-module over a ring `R` satisfying the strong rank condition is a finite number.
|
Basis.le_span
theorem Basis.le_span :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type w}
[inst_3 : RankCondition R] {J : Set M} (v : Basis ι R M),
Submodule.span R J = ⊤ → Cardinal.mk ↑(Set.range ⇑v) ≤ Cardinal.mk ↑J
This theorem states that, for a given ring `R` that satisfies the rank condition and a set `M` under the conditions of being an additive commutative group and an `R`-module, the cardinality of any basis (denoted by `v`) is bounded by the cardinality of any set `J` that spans `M`. In other words, if we take `J` such that its span is the entire module `M` (denoted by `⊤`), then the cardinality of the range of `v` (which forms a basis) is less than or equal to the cardinality of `J`. This is a formal statement of the intuitive idea in linear algebra that a basis of a vector space can't have more elements than any set that spans the vector space.
More concisely: For any commutative ring `R` satisfying the rank condition, an additive commutative group and `R`-module `M` with a spanning set `J` of finite cardinality, the cardinality of a basis for `M` is less than or equal to the cardinality of `J`.
|
rank_lt_aleph0
theorem 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] [inst_4 : Module.Finite R M], Module.rank R M < Cardinal.aleph0
The theorem `rank_lt_aleph0` states that for any type `R` and `M`, given `R` is a ring, `M` is an additive commutative group, `M` is a module over `R`, `R` satisfies the strong rank condition and `M` is a finite module over `R`, the rank of the module `M` is less than `ℵ₀`, the smallest infinite cardinal. In other words, the rank of a finite module is always finite.
More concisely: The rank of a finite module over a ring satisfying the strong rank condition is a finite number.
|