mathlib documentation

data.polynomial.inductions

Induction on polynomials #

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

source
noncomputable def polynomial.div_X {R : Type u} [semiring R] (p : R[X]) :
R[X]

div_X 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

Equations
source
@[simp]
theorem polynomial.coeff_div_X {R : Type u} {n : ℕ} [semiring R] {p : R[X]} :
p.div_X.coeff n = p.coeff (n + 1)
source
theorem polynomial.div_X_mul_X_add {R : Type u} [semiring R] (p : R[X]) :
(p.div_X) * polynomial.X + ⇑polynomial.C (p.coeff 0) = p
source
@[simp]
theorem polynomial.div_X_C {R : Type u} [semiring R] (a : R) :
(⇑polynomial.C a).div_X = 0
source
theorem polynomial.div_X_eq_zero_iff {R : Type u} [semiring R] {p : R[X]} :
p.div_X = 0 ↔ p = ⇑polynomial.C (p.coeff 0)
source
theorem polynomial.div_X_add {R : Type u} [semiring R] {p q : R[X]} :
(p + q).div_X = p.div_X + q.div_X
source
theorem polynomial.degree_div_X_lt {R : Type u} [semiring R] {p : R[X]} (hp0 : p ≠ 0) :
p.div_X.degree < p.degree
source
noncomputable def polynomial.rec_on_horner {R : Type u} [semiring R] {M : R[X] → Sort u_1} (p : R[X]) :
M 0 → (Π (p : R[X]) (a : R), p.coeff 0 = 0 → a ≠ 0 → M p → M (p + ⇑polynomial.C a)) → (Π (p : R[X]), p ≠ 0 → M p → M (p * polynomial.X)) → M p

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

Equations
source
theorem polynomial.degree_pos_induction_on {R : Type u} [semiring R] {P : R[X] → Prop} (p : R[X]) (h0 : 0 < p.degree) (hC : ∀ {a : R}, a ≠ 0 → P ((⇑polynomial.C a) * polynomial.X)) (hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * polynomial.X)) (hadd : ∀ {p : R[X]} {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 nat_degree_ne_zero_induction_on for a similar statement involving no explicit multiplication.

source
theorem polynomial.nat_degree_ne_zero_induction_on {R : Type u} [semiring R] {M : R[X] → Prop} {f : R[X]} (f0 : f.nat_degree ≠ 0) (h_C_add : ∀ {a : R} {p : R[X]}, M p → M (⇑polynomial.C a + p)) (h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)) (h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (⇑(polynomial.monomial n) a)) :
M f

A property holds for all polynomials of non-zero nat_degree 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.