monotone_stabilizes_iff_noetherian

English

A module M is Noetherian iff every increasing chain of submodules stabilizes (i.e., becomes constant after some finite stage).

Русский

Модуль M — Нётеров тогда и только тогда, когда любая возрастающая цепь подмодулей стабилизируется (становится постоянной после некоторого конечного шага).

LaTeX

$$$(\\forall f: \\mathbb{N} \\to_o \\mathrm{Submodule}_R(M), \\exists n, \\forall m \\ge n, f(n)=f(m)) \\iff \\ \\operatorname{IsNoetherian}(R,M)$$$

Lean4

/-- A module is Noetherian iff every increasing chain of submodules stabilizes. -/
theorem monotone_stabilizes_iff_noetherian :
    (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by
  rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]

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