length — Mathlib

English

The length of a module is defined as the Krull dimension of its submodule lattice (lifted to ENat).

Русский

Длина модуля определяется как крулль-измерение решетки подмодулов (в виде ENat).

LaTeX

$$$\operatorname{length}(R,M) = \operatorname{unbot}(\operatorname{krullDim}(\operatorname{Submodule}_R M)).$$$

Lean4

/-- The length of a module, defined as the krull dimension of its submodule lattice. -/
noncomputable def length : ℕ∞ :=
  (Order.krullDim (Submodule R M)).unbot (by simp [Order.krullDim_eq_bot_iff])

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