Nilpotent elements in quotient rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem ideal.is_radical_iff_quotient_reduced {R : Type u_1} [comm_ring R] (I : ideal R) :

theorem ideal.is_nilpotent.induction_on {S : Type u_2} [comm_ring S] (I : ideal S) (hI : is_nilpotent I) {P : Π ⦃S : Type u_2⦄ [_inst_4 : comm_ring S], ideal S → Prop} (h₁ : ∀ ⦃S : Type u_2⦄ [_inst_5 : comm_ring S] (I : ideal S), I ^ 2 = ⊥ → P I) (h₂ : ∀ ⦃S : Type u_2⦄ [_inst_6 : comm_ring 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 is_nilpotent.is_unit_quotient_mk_iff {R : Type u_1} [comm_ring R] {I : ideal R} (hI : is_nilpotent I) {x : R} :