HepLean Documentation
Mathlib
.
RingTheory
.
Ideal
.
Quotient
.
Noetherian
Search
Google site search
return to top
source
Imports
Init
Mathlib.RingTheory.Noetherian
Mathlib.RingTheory.Ideal.Quotient.Operations
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
⋯
=
⋯