mathlib3 documentation


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_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 ( ( I) J) P J) :

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.