length_ne_top — Mathlib

English

If M is Artinian and Noetherian, then length R M is not top.

Русский

Если модуль Артинский и Ноetherский, то длина модуля не равна топу.

LaTeX

$$[IsArtinian R M] [IsNoetherian R M] ⇒ \operatorname{length}(R,M) \neq \top.$$

Lean4

theorem length_ne_top [IsArtinian R M] [IsNoetherian R M] : Module.length R M ≠ ⊤ :=
  by
  rw [length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian]
  exact ⟨‹_›, ‹_›⟩

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