instIsNoetherianRingLocalization — Mathlib

English

If R is a Noetherian ring, then Localization by any submonoid S is Noetherian; i.e., the localization of a Noetherian ring is Noetherian.

Русский

Если R — локальное кольцо Ноetherово, то Localization(S) тоже Ноetherово.

LaTeX

$$instIsNoetherianRingLocalization : IsNoetherianRing (Localization S)$$

Lean4

instance {R} [CommRing R] [IsNoetherianRing R] (S : Submonoid R) : IsNoetherianRing (Localization S) :=
  IsLocalization.isNoetherianRing S _ ‹_›

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