IsNoetherian.rank_lt_aleph0
theorem IsNoetherian.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 `IsNoetherian.rank_lt_aleph0` states that for any given ring `R` and any given module `M` over this ring, where the ring `R` satisfies the strong rank condition and the module `M` is finite, the rank of the module `M` is strictly less than `ℵ₀` (aleph null), which is the smallest infinite cardinal number. In other words, the rank of a finite module over a ring with the strong rank condition is finite.
More concisely: For any ring satisfying the strong rank condition and any finite module over it, the module's rank is a finite number strictly less than aleph null (the smallest infinite cardinal number).
|
IsNoetherian.iff_rank_lt_aleph0
theorem IsNoetherian.iff_rank_lt_aleph0 :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
IsNoetherian K V ↔ Module.rank K V < Cardinal.aleph0
This theorem states that for any division ring 'K' and any additive commutative group 'V' that is also a module over 'K', 'V' is Noetherian if and only if the rank of 'V' as a module over 'K' is strictly less than the first infinite cardinal number, denoted as `ℵ₀`. In other words, a module over a division ring is Noetherian iff its dimension (as a cardinal) is finite.
More concisely: A module over a division ring is Noetherian if and only if its rank (as a cardinal) is finite.
|
IsNoetherian.finite_basis_index
theorem IsNoetherian.finite_basis_index :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
{s : Set ι} [inst_3 : IsNoetherian K V], Basis (↑s) K V → s.Finite
The theorem, `IsNoetherian.finite_basis_index`, states that for any division ring `K` and any additively commutative group (module) `V` over `K`, if `V` is a Noetherian module, then for any basis of `V` that is indexed by a set `s`, `s` must be finite. In other words, in a Noetherian module over a division ring, if a basis is indexed by a set, that set is necessarily finite.
More concisely: In a Noetherian module over a division ring, every basis has a finite indexing set.
|
IsNoetherian.iff_fg
theorem IsNoetherian.iff_fg :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
IsNoetherian K V ↔ Module.Finite K V
This theorem states that for any module `V` over a division ring `K`, the module is Noetherian if and only if it is finitely generated. In mathematical terms, a Noetherian module is one where every submodule is finitely generated, and this theorem states that such a property is equivalent to the module itself being finitely generated. The theorem applies to any type `K` that forms a division ring and any type `V` that forms an additive commutative group and a module over `K`.
More concisely: A module over a division ring is Noetherian if and only if it is finitely generated.
|