TorchLean API
Docs Home
Guide
Examples
Graphs
Mathlib
.
RingTheory
.
Ideal
.
Quotient
.
Noetherian
Search
Declaration colors
def
theorem
structure
axiom
return to top
source
Imports
Init
Mathlib.RingTheory.Noetherian.Basic
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
)