length_eq_height — Mathlib

English

The length of a module equals the height of the top submodule, i.e., the entire submodule lattice's maximal chain length.

Русский

Длина модуля равна высоте верхнего подмодуля, то есть длине максимальной цепочки подмодулов.

LaTeX

$$$\operatorname{length}(R,M) = \operatorname{height}(\top : \text{Submodule}_R M).$$$

Lean4

theorem length_eq_height : Module.length R M = Order.height (⊤ : Submodule R M) :=
  by
  apply WithBot.coe_injective
  rw [Module.coe_length, Order.height_top_eq_krullDim]

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