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 S → Prop} (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 ≤ 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_3} [CommRing R] {I : Ideal R} (hI : IsNilpotent I) {x : R} : IsUnit ((Ideal.Quotient.mk I) x) ↔ IsUnit x