Nilpotent elements in quotient rings

theorem Ideal.isRadical_iff_quotient_reduced {R : Type u_1} [CommRing R] (I : Ideal R) : Ideal.IsRadical I ↔ 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 S inst I) (h₂ : ⦃S : Type u_2⦄ → [inst : CommRing S] → (I J : Ideal S) → I ≤ J → P S inst I → P (S ⧸ I) (Ideal.Quotient.commRing I) (Ideal.map (Ideal.Quotient.mk I) J) → P S inst J) : P S inst✝ 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