Documentation
Schlessinger
.
Mathlib
.
RingTheory
.
PowerSeries
.
Noetherian
Search
return to top
source
Imports
Init
Mathlib.RingTheory.Noetherian.Defs
Mathlib.RingTheory.PowerSeries.Basic
Imported by
instIsNoetherianRingPowerSeries_schlessinger
source
instance
instIsNoetherianRingPowerSeries_schlessinger
(
R
:
Type
u_1)
[
CommRing
R
]
[
IsNoetherianRing
R
]
:
IsNoetherianRing
(
PowerSeries
R
)