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 {S : Type u_1} [CommRing S] (I : Ideal S) (hI : IsNilpotent I) {P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop} (h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I) (h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (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.

theorem IsNilpotent.isUnit_quotient_mk_iff {R : Type u_2} [CommRing R] {I : Ideal R} (hI : IsNilpotent I) {x : R} : IsUnit ((Ideal.Quotient.mk I) x) ↔ IsUnit x