Documentation

Mathlib.Algebra.Polynomial.Inductions

Induction on polynomials #

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

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
  • p.divX = { toFinsupp := p.toFinsupp.divOf 1 }
Instances For
    @[simp]
    theorem Polynomial.coeff_divX {R : Type u} {n : } [Semiring R] {p : Polynomial R} :
    p.divX.coeff n = p.coeff (n + 1)
    theorem Polynomial.divX_mul_X_add {R : Type u} [Semiring R] (p : Polynomial R) :
    p.divX * Polynomial.X + Polynomial.C (p.coeff 0) = p
    @[simp]
    theorem Polynomial.X_mul_divX_add {R : Type u} [Semiring R] (p : Polynomial R) :
    Polynomial.X * p.divX + Polynomial.C (p.coeff 0) = p
    @[simp]
    theorem Polynomial.divX_C {R : Type u} [Semiring R] (a : R) :
    (Polynomial.C a).divX = 0
    theorem Polynomial.divX_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} :
    p.divX = 0 p = Polynomial.C (p.coeff 0)
    theorem Polynomial.divX_add {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
    (p + q).divX = p.divX + q.divX
    @[simp]
    @[simp]
    @[simp]
    theorem Polynomial.divX_C_mul {R : Type u} {a : R} [Semiring R] {p : Polynomial R} :
    (Polynomial.C a * p).divX = Polynomial.C a * p.divX
    theorem Polynomial.divX_X_pow {R : Type u} {n : } [Semiring R] :
    (Polynomial.X ^ n).divX = if n = 0 then 0 else Polynomial.X ^ (n - 1)
    noncomputable def Polynomial.divX_hom {R : Type u} [Semiring R] :

    divX as an additive homomorphism.

    Equations
    • Polynomial.divX_hom = { toFun := Polynomial.divX, map_zero' := , map_add' := }
    Instances For
      @[simp]
      theorem Polynomial.divX_hom_toFun {R : Type u} [Semiring R] {p : Polynomial R} :
      Polynomial.divX_hom p = p.divX
      theorem Polynomial.natDegree_divX_eq_natDegree_tsub_one {R : Type u} [Semiring R] {p : Polynomial R} :
      p.divX.natDegree = p.natDegree - 1
      theorem Polynomial.natDegree_divX_le {R : Type u} [Semiring R] {p : Polynomial R} :
      p.divX.natDegree p.natDegree
      theorem Polynomial.divX_C_mul_X_pow {R : Type u} {a : R} {n : } [Semiring R] :
      (Polynomial.C a * Polynomial.X ^ n).divX = 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) :
      p.divX.degree < p.degree
      @[irreducible]
      noncomputable def Polynomial.recOnHorner {R : Type u} [Semiring R] {M : Polynomial RSort u_1} (p : Polynomial R) (M0 : M 0) (MC : (p : Polynomial R) → (a : R) → p.coeff 0 = 0a 0M pM (p + Polynomial.C a)) (MX : (p : Polynomial R) → 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} [Semiring R] {P : Polynomial RProp} (p : Polynomial R) (h0 : 0 < p.degree) (hC : ∀ {a : R}, a 0P (Polynomial.C a * Polynomial.X)) (hX : ∀ {p : Polynomial R}, 0 < p.degreeP pP (p * Polynomial.X)) (hadd : ∀ {p : Polynomial R} {a : R}, 0 < p.degreeP 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} [Semiring R] {M : Polynomial RProp} {f : Polynomial R} (f0 : f.natDegree 0) (h_C_add : ∀ {a : R} {p : Polynomial R}, M pM (Polynomial.C a + p)) (h_add : ∀ {p q : Polynomial R}, M pM qM (p + q)) (h_monomial : ∀ {n : } {a : R}, a 0n 0M ((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.