Theorems · Theorem · field theory

Polynomial.induction_with_natDegree_le

∀ {R : Type u_1} [inst : Semiring R] (motive : Polynomial R → Prop) (N : ℕ),
  motive 0 →
    (∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (Polynomial.C r * Polynomial.X ^ n)) →
      (∀ (f g : Polynomial R), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)) →
        ∀ (f : Polynomial R), f.natDegree ≤ N → motive f

An induction lemma for polynomials. It takes a natural number N as a parameter, that is required to be at least as big as the natDegree of the polynomial. This is useful to prove results where you want to change each term in a polynomial to something else depending on the natDegree of the polynomial itself and not on the specific natDegree of each term.

Defined in

Mathlib.Algebra.Polynomial.EraseLead

Cited by

4 results in Mathlib

Foundations

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

Assumes

Semiring