# Documentation

Mathlib.Data.Polynomial.Inductions

# Induction on polynomials #

This file contains lemmas dealing with different flavours of induction on polynomials.

def Polynomial.divX {R : Type u} [] (p : ) :

divX p returns a polynomial q such that q * X + C (p.coeff 0) = p. It can be used in a semiring where the usual division algorithm is not possible

Instances For
@[simp]
theorem Polynomial.coeff_divX {R : Type u} {n : } [] {p : } :
theorem Polynomial.divX_mul_X_add {R : Type u} [] (p : ) :
* Polynomial.X + Polynomial.C () = p
@[simp]
theorem Polynomial.X_mul_divX_add {R : Type u} [] (p : ) :
Polynomial.X * + Polynomial.C () = p
@[simp]
theorem Polynomial.divX_C {R : Type u} [] (a : R) :
Polynomial.divX (Polynomial.C a) = 0
theorem Polynomial.divX_eq_zero_iff {R : Type u} [] {p : } :
p = Polynomial.C ()
theorem Polynomial.divX_add {R : Type u} [] {p : } {q : } :
@[simp]
theorem Polynomial.divX_zero {R : Type u} [] :
@[simp]
theorem Polynomial.divX_one {R : Type u} [] :
@[simp]
theorem Polynomial.divX_C_mul {R : Type u} {a : R} [] {p : } :
Polynomial.divX (Polynomial.C a * p) = Polynomial.C a *
theorem Polynomial.divX_X_pow {R : Type u} {n : } [] :
Polynomial.divX (Polynomial.X ^ n) = if n = 0 then 0 else Polynomial.X ^ (n - 1)
noncomputable def Polynomial.divX_hom {R : Type u} [] :

divX as an additive homomorphism.

Instances For
@[simp]
theorem Polynomial.divX_hom_toFun {R : Type u} [] {p : } :
Polynomial.divX_hom p =
theorem Polynomial.natDegree_divX_le {R : Type u} [] {p : } :
theorem Polynomial.divX_C_mul_X_pow {R : Type u} {a : R} {n : } [] :
Polynomial.divX (Polynomial.C a * Polynomial.X ^ n) = if n = 0 then 0 else Polynomial.C a * Polynomial.X ^ (n - 1)
theorem Polynomial.degree_divX_lt {R : Type u} [] {p : } (hp0 : p 0) :
noncomputable def Polynomial.recOnHorner {R : Type u} [] {M : Sort u_1} (p : ) (M0 : M 0) (MC : (p : ) → (a : R) → = 0a 0M pM (p + Polynomial.C a)) (MX : (p : ) → p 0M pM (p * Polynomial.X)) :
M p

An induction principle for polynomials, valued in Sort* instead of Prop.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Polynomial.degree_pos_induction_on {R : Type u} [] {P : } (p : ) (h0 : ) (hC : {a : R} → a 0P (Polynomial.C a * Polynomial.X)) (hX : {p : } → P pP (p * Polynomial.X)) (hadd : {p : } → {a : R} → P pP (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.

theorem Polynomial.natDegree_ne_zero_induction_on {R : Type u} [] {M : } {f : } (f0 : ) (h_C_add : {a : R} → {p : } → M pM (Polynomial.C a + p)) (h_add : {p q : } → M pM qM (p + q)) (h_monomial : {n : } → {a : R} → a 0n 0M (↑() a)) :
M f

A property holds for all polynomials of non-zero natDegree with coefficients in a semiring R if it holds for

• p + a, with a ∈ R, p ∈ R[X],
• p + q, with p, q ∈ R[X],
• monomials with nonzero coefficient and non-zero exponent, with appropriate restrictions on each term. Note that multiplication is "hidden" in the assumption on monomials, so there is no explicit multiplication in the statement. See degree_pos_induction_on for a similar statement involving more explicit multiplications.