Documentation

Mathlib.RingTheory.Noetherian.Nilpotent

Nilpotent ideals in Noetherian rings #

Main results #

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