Theorems · Theorem · field theory

Polynomial.degree_pos_induction_on

∀ {R : Type u} [inst : Semiring R] {P : Polynomial R → Prop} (p : Polynomial R),
  0 < p.degree →
    (∀ {a : R}, a ≠ 0 → P (Polynomial.C a * Polynomial.X)) →
      (∀ {p : Polynomial R}, 0 < p.degree → P p → P (p * Polynomial.X)) →
        (∀ {p : Polynomial R} {a : R}, 0 < p.degree → P p → P (p + Polynomial.C a)) → P p

A property holds for all polynomials of positive degree with coefficients in a semiring R if it holds for * a * X, with a ∈ R, * p * X, with p ∈ R[X], * p + a, with a ∈ R, p ∈ R[X], with appropriate restrictions on each term. See natDegree_ne_zero_induction_on for a similar statement involving no explicit multiplication.

Defined in

Mathlib.Algebra.Polynomial.Inductions

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring