Nilpotence in ring quotients

An element nilpotent modulo a two-sided ideal remains nilpotent modulo every power of that ideal. This allows a representation kernel to be refined by taking powers without losing nilpotence of its operators. The ring need not be commutative.

For commutative rings, the quotient by the nilradical is reduced.

instance Ado.isReduced_quotient_nilradical (A : Type u_1) [CommRing A] : IsReduced (A ⧸ nilradical A)

The quotient of a commutative ring by its nilradical is reduced.

theorem Ideal.isNilpotent_quotient_pow_of_isNilpotent_quotient {A : Type u_1} [Ring A] (I : Ideal A) [I.IsTwoSided] {a : A} (ha : IsNilpotent ((Quotient.mk I) a)) (n : ℕ) : IsNilpotent ((Quotient.mk (I ^ n)) a)

An element nilpotent modulo a two-sided ideal remains nilpotent modulo every power of it, including the zeroth power.