length_ne_top_iff_finiteDimensionalOrder

English

length R M ≠ ⊤ iff FiniteDimensionalOrder(Submodule R M).

Русский

length R M не равна ⊤ тогда и только тогда, когда решетка подмодулов конечнодименсионна.

LaTeX

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

Lean4

theorem length_ne_top_iff_finiteDimensionalOrder : length R M ≠ ⊤ ↔ FiniteDimensionalOrder (Submodule R M) := by
  rw [Ne, length_eq_top_iff_infiniteDimensionalOrder, ← not_finiteDimensionalOrder_iff, not_not]

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