English
Let R be a semiring and M an R-module. Then M is Noetherian if and only if the submodules of M, ordered by the strict inclusion relation (i.e., greater-than corresponds to proper inclusion), form a well-founded relation. Equivalently, there is no infinite strictly descending chain of submodules.
Русский
Пусть R — полусколь, M — модуль над R. Тогда M — это Нётеров модуль тогда и только тогда, когда множество подмодулей M, упорядоченных по отношению строгого включения, образует хорошо основанный порядок. Эквивалентно отсутствию бесконечной последовательности подмножеств с строгим включением.
LaTeX
$$$\\text{IsNoetherian}(R,M) \\iff \\operatorname{WellFounded}\\big((\\cdot > \\cdot) : \\text{Submodule}_R(M) \\to \\text{Submodule}_R(M) \\to \\operatorname{Prop}\\big)$$$
Lean4
theorem isNoetherian_iff : IsNoetherian R M ↔ WellFounded ((· > ·) : Submodule R M → Submodule R M → Prop) := by
rw [isNoetherian_iff', ← isWellFounded_iff]
