Nilpotent ideals in Noetherian rings

Main results

• IsNoetherianRing.isNilpotent_nilradical

theorem IsNoetherianRing.isNilpotent_nilradical (R : Type u_1) [CommSemiring R] [IsNoetherianRing R] : IsNilpotent (nilradical R)

theorem Ideal.FG.isNilpotent_iff_le_nilradical {R : Type u_1} [CommSemiring R] {I : Ideal R} (hI : I.FG) : IsNilpotent I ↔ I ≤ nilradical R