isNoetherian_of_submodule_of_noetherian

English

If N is a submodule of M and M is Noetherian, then N is Noetherian.

Русский

Если N является подмодулем M, а M — Ноетеров, то и N Ноетеров.

LaTeX

$$$IsNoetherian(R,N)$ given $IsNoetherian(R,M)$ and $N \le M$$$

Lean4

theorem isNoetherian_of_submodule_of_noetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M)
    (h : IsNoetherian R M) : IsNoetherian R N :=
  isNoetherian_mk ⟨OrderEmbedding.wellFounded (Submodule.MapSubtype.orderEmbedding N).dual h.wf⟩

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