isNoetherian_submodule' — Mathlib

English

There exists a well-founded order on submodules that characterizes Noetherian property, providing a practical equivalence.

Русский

Существуют условия, при которых Ноетерова свойство эквивалентно существованию хорошо-построенного порядка на подмодулях.

LaTeX

$$$IsNoetherian(R,M) \iff WellFoundedGT(Submodule(R,M))$$$

Lean4

instance isNoetherian_submodule' [IsNoetherian R M] (N : Submodule R M) : IsNoetherian R N :=
  isNoetherian_submodule.2 fun _ _ => IsNoetherian.noetherian _

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