Documentation

Mathlib.RingTheory.QuotientNilpotent

Nilpotent elements in quotient rings #

theorem Ideal.isRadical_iff_quotient_reduced {R : Type u_1} [CommRing R] (I : Ideal R) :
I.IsRadical IsReduced (R I)
theorem Ideal.IsNilpotent.induction_on {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [Algebra R S] (I : Ideal S) (hI : IsNilpotent I) {P : S : Type u_2⦄ → [inst : CommRing S] → Ideal SProp} (h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = P I) (h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I JP IP (Ideal.map (Ideal.Quotient.mk I) J)P J) :
P I

Let P be a property on ideals. If P holds for square-zero ideals, and if P I → P (J ⧸ I) → P J, then P holds for all nilpotent ideals.