isNoetherian_of_subsingleton — Mathlib

English

If M is Noetherian as an R-module, then any submodule N ≤ M is Noetherian as an R-module.

Русский

Если модуль M является Ноетеровым как R-модуль, то любой подмодуль N ⊆ M также Ноетеров.

LaTeX

$$$\text{If } IsNoetherian(R,M) \text{ and } N \le M,\ text{ then } IsNoetherian(R,N)$$$

Lean4

/-- Modules over the trivial ring are Noetherian. -/
instance (priority := 100) isNoetherian_of_subsingleton (R M) [Subsingleton R] [Semiring R] [AddCommMonoid M]
    [Module R M] : IsNoetherian R M :=
  haveI := Module.subsingleton R M
  isNoetherian_of_finite R M

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