Induction on polynomials

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

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

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

Equations

• Polynomial.divX p = { toFinsupp := AddMonoidAlgebra.divOf p.toFinsupp 1 }

@[simp]

theorem Polynomial.coeff_divX {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : Polynomial.coeff (Polynomial.divX p) n = Polynomial.coeff p (n + 1)

theorem Polynomial.divX_mul_X_add {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.divX p * Polynomial.X + Polynomial.C (Polynomial.coeff p 0) = p

@[simp]

theorem Polynomial.X_mul_divX_add {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.X * Polynomial.divX p + Polynomial.C (Polynomial.coeff p 0) = p

@[simp]

theorem Polynomial.divX_C {R : Type u} [Semiring R] (a : R) : Polynomial.divX (Polynomial.C a) = 0

theorem Polynomial.divX_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.divX p = 0 ↔ p = Polynomial.C (Polynomial.coeff p 0)

theorem Polynomial.divX_add {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} : Polynomial.divX (p + q) = Polynomial.divX p + Polynomial.divX q

@[simp]

theorem Polynomial.divX_zero {R : Type u} [Semiring R] : Polynomial.divX 0 = 0

@[simp]

theorem Polynomial.divX_one {R : Type u} [Semiring R] : Polynomial.divX 1 = 0

@[simp]

theorem Polynomial.divX_C_mul {R : Type u} {a : R} [Semiring R] {p : Polynomial R} : Polynomial.divX (Polynomial.C a * p) = Polynomial.C a * Polynomial.divX p

theorem Polynomial.divX_X_pow {R : Type u} {n : ℕ} [Semiring R] : Polynomial.divX (Polynomial.X ^ n) = if n = 0 then 0 else Polynomial.X ^ (n - 1)

noncomputable def Polynomial.divX_hom {R : Type u} [Semiring R] : Polynomial R →+ Polynomial R

divX as an additive homomorphism.

Equations

• Polynomial.divX_hom = { toZeroHom := { toFun := Polynomial.divX, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem Polynomial.divX_hom_toFun {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.divX_hom p = Polynomial.divX p

theorem Polynomial.natDegree_divX_eq_natDegree_tsub_one {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.natDegree (Polynomial.divX p) = Polynomial.natDegree p - 1

theorem Polynomial.natDegree_divX_le {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.natDegree (Polynomial.divX p) ≤ Polynomial.natDegree p

theorem Polynomial.divX_C_mul_X_pow {R : Type u} {a : R} {n : ℕ} [Semiring R] : 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} [Semiring R] {p : Polynomial R} (hp0 : p ≠ 0) : Polynomial.degree (Polynomial.divX p) < Polynomial.degree p

noncomputable def Polynomial.recOnHorner {R : Type u} [Semiring R] {M : Polynomial R → Sort u_1} (p : Polynomial R) (M0 : M 0) (MC : (p : Polynomial R) → (a : R) → Polynomial.coeff p 0 = 0 → a ≠ 0 → M p → M (p + Polynomial.C a)) (MX : (p : Polynomial R) → p ≠ 0 → M p → M (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.

theorem Polynomial.degree_pos_induction_on {R : Type u} [Semiring R] {P : Polynomial R → Prop} (p : Polynomial R) (h0 : 0 < Polynomial.degree p) (hC : ∀ {a : R}, a ≠ 0 → P (Polynomial.C a * Polynomial.X)) (hX : ∀ {p : Polynomial R}, 0 < Polynomial.degree p → P p → P (p * Polynomial.X)) (hadd : ∀ {p : Polynomial R} {a : R}, 0 < Polynomial.degree p → 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.

theorem Polynomial.natDegree_ne_zero_induction_on {R : Type u} [Semiring R] {M : Polynomial R → Prop} {f : Polynomial R} (f0 : Polynomial.natDegree f ≠ 0) (h_C_add : ∀ {a : R} {p : Polynomial R}, M p → M (Polynomial.C a + p)) (h_add : ∀ {p q : Polynomial R}, 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 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.