length_lt — Mathlib

English

If N ≠ ⊤, then Module.length R N < Module.length R M.

Русский

Если N не равен ⊤, тогда длина N меньше длины M.

LaTeX

$$$N \neq \top \Rightarrow \operatorname{length}(R,N) < \operatorname{length}(R,M).$$$

Lean4

theorem length_lt [IsArtinian R M] [IsNoetherian R M] {N : Submodule R M} (h : N ≠ ⊤) :
    Module.length R N < Module.length R M := by
  simpa [← Module.length_top (M := M), Module.length_submodule] using height_strictMono h.lt_top

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