Theorems · Theorem · commutative algebra

FreeCommRing.induction_on

∀ {α : Type u} {motive : FreeCommRing α → Prop} (z : FreeCommRing α),
  motive (-1) →
    (∀ (b : α), motive (FreeCommRing.of b)) →
      (∀ (x y : FreeCommRing α), motive x → motive y → motive (x + y)) →
        (∀ (x y : FreeCommRing α), motive x → motive y → motive (x * y)) → motive z

Defined in

Mathlib.RingTheory.FreeCommRing

Cited by

4 results in Mathlib

Foundations

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