Theorems · Theorem · commutative algebra

Ideal.IsNilpotent.induction_on

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

Defined in

Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Cited by

3 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing