length_eq_top_iff_infiniteDimensionalOrder

English

The length equals top iff the submodule lattice has infinite dimensional order.

Русский

Длина равна верхнему пределу тогда и только тогда, когда решетка подмодулов имеет бесконечное размерное упорядочение.

LaTeX

$$$\operatorname{length}(R,M) = \top \iff \operatorname{InfiniteDimensionalOrder}(\operatorname{Submodule}_R M).$$$

Lean4

theorem length_eq_top_iff_infiniteDimensionalOrder : length R M = ⊤ ↔ InfiniteDimensionalOrder (Submodule R M) := by
  rw [← WithBot.coe_inj, WithBot.coe_top, coe_length, Order.krullDim_eq_top_iff, ← not_finiteDimensionalOrder_iff]

Похожие утверждения