Documentation
Mathlib
.
RingTheory
.
Ideal
.
Quotient
.
Noetherian
Search
return to top
source
Imports
Init
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Ideal.Quotient.Operations
Imported by
Ideal
.
Quotient
.
isNoetherianRing
← Copula mathematical handbook
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
)