doc-next-gen

Mathlib.RingTheory.Ideal.Quotient.Noetherian

Module docstring

{"# Noetherian quotient rings and quotient modules "}

Ideal.Quotient.isNoetherianRing instance
{R : Type*} [CommRing R] [IsNoetherianRing R] (I : Ideal R) : IsNoetherianRing (R ⧸ I)
Full source 
instance Ideal.Quotient.isNoetherianRing {R : Type*} [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) : IsNoetherianRing (R ⧸ I) :=
  isNoetherianRing_iff.mpr <| isNoetherian_of_tower R <| inferInstance
Noetherian Property of Quotient Rings
Informal description
For any commutative Noetherian ring $R$ and any ideal $I$ of $R$, the quotient ring $R/I$ is also Noetherian.