Theorems · Theorem · field theory

Polynomial.induction_on

∀ {R : Type u} [inst : Semiring R] {motive : Polynomial R → Prop} (p : Polynomial R),
  (∀ (a : R), motive (Polynomial.C a)) →
    (∀ (p q : Polynomial R), motive p → motive q → motive (p + q)) →
      (∀ (n : ℕ) (a : R),
          motive (Polynomial.C a * Polynomial.X ^ n) → motive (Polynomial.C a * Polynomial.X ^ (n + 1))) →
        motive p

Defined in

Mathlib.Algebra.Polynomial.Basic

Cited by

23 results in Mathlib

Foundations

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

Assumes

Semiring