Documentation
Mathlib
.
RingTheory
.
QuotientNoetherian
Search
Google site search
Mathlib
.
RingTheory
.
QuotientNoetherian
source
Imports
Init
Mathlib.RingTheory.Noetherian
Mathlib.RingTheory.QuotientNilpotent
Imported by
Ideal
.
Quotient
.
isNoetherianRing
Noetherian quotient rings and quotient modules
#
source
instance
Ideal
.
Quotient
.
isNoetherianRing
{R :
Type
u_1}
[
CommRing
R
]
[
IsNoetherianRing
R
]
(I :
Ideal
R
)
:
IsNoetherianRing
(
R
⧸
I
)
Equations
@
Ideal.Quotient.isNoetherianRing
=
@
Ideal.Quotient.isNoetherianRing.proof_1