Documentation
Mathlib
.
RingTheory
.
Noetherian
.
Nilpotent
Search
return to top
source
Imports
Init
Mathlib.RingTheory.Finiteness.Ideal
Mathlib.RingTheory.Nilpotent.Lemmas
Mathlib.RingTheory.Noetherian.Defs
Imported by
IsNoetherianRing
.
isNilpotent_nilradical
Ideal
.
FG
.
isNilpotent_iff_le_nilradical
Nilpotent ideals in Noetherian rings
#
Main results
#
IsNoetherianRing.isNilpotent_nilradical
source
theorem
IsNoetherianRing
.
isNilpotent_nilradical
(
R
:
Type
u_1)
[
CommSemiring
R
]
[
IsNoetherianRing
R
]
:
IsNilpotent
(
nilradical
R
)
source
theorem
Ideal
.
FG
.
isNilpotent_iff_le_nilradical
{
R
:
Type
u_1}
[
CommSemiring
R
]
{
I
:
Ideal
R
}
(
hI
:
I
.
FG
)
:
IsNilpotent
I
↔
I
≤
nilradical
R