isNoetherianRing — Mathlib

English

If R is Noetherian, and S is a localization of R with respect to a submonoid M, then S is Noetherian.

Русский

Если R — ноetherово кольцо и S является локализацией по подмономоду M, то S также Ноetherово.

LaTeX

$$isNoetherianRing (h : IsNoetherianRing R) : IsNoetherianRing S$$

Lean4

theorem isNoetherianRing (h : IsNoetherianRing R) : IsNoetherianRing S :=
  by
  rw [isNoetherianRing_iff, isNoetherian_iff] at h ⊢
  exact OrderEmbedding.wellFounded (IsLocalization.orderEmbedding M S).dual h

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