Documentation

Mathlib.Data.Polynomial.Degree.TrailingDegree

Trailing degree of univariate polynomials #

Main definitions #

Converts most results about degree, natDegree and leadingCoeff to results about the bottom end of a polynomial

trailingDegree p is the multiplicity of x in the polynomial p, i.e. the smallest X-exponent in p. trailingDegree p = some n when p ≠ 0 and n is the smallest power of X that appears in p, otherwise trailingDegree 0 = ⊤.

Equations
Instances For

    trailingCoeff p gives the coefficient of the smallest power of X in p

    Equations
    Instances For

      a polynomial is monic_at if its trailing coefficient is 1

      Equations
      Instances For
        Equations
        • Polynomial.TrailingMonic.decidable = inferInstance
        @[simp]
        theorem Polynomial.trailingDegree_monomial {R : Type u} {a : R} {n : } [Semiring R] (ha : a 0) :
        @[simp]
        theorem Polynomial.trailingDegree_C {R : Type u} {a : R} [Semiring R] (ha : a 0) :
        Polynomial.trailingDegree (Polynomial.C a) = 0
        theorem Polynomial.le_trailingDegree_C {R : Type u} {a : R} [Semiring R] :
        0 Polynomial.trailingDegree (Polynomial.C a)
        @[simp]
        theorem Polynomial.natTrailingDegree_C {R : Type u} [Semiring R] (a : R) :
        Polynomial.natTrailingDegree (Polynomial.C a) = 0
        @[simp]
        theorem Polynomial.trailingDegree_C_mul_X_pow {R : Type u} {a : R} [Semiring R] (n : ) (ha : a 0) :
        Polynomial.trailingDegree (Polynomial.C a * Polynomial.X ^ n) = n
        theorem Polynomial.le_trailingDegree_C_mul_X_pow {R : Type u} [Semiring R] (n : ) (a : R) :
        n Polynomial.trailingDegree (Polynomial.C a * Polynomial.X ^ n)
        theorem Polynomial.le_natTrailingDegree {R : Type u} {n : } [Semiring R] {p : Polynomial R} (hp : p 0) (hn : ∀ (m : ), m < nPolynomial.coeff p m = 0) :
        def Polynomial.nextCoeffUp {R : Type u} [Semiring R] (p : Polynomial R) :
        R

        The second-lowest coefficient, or 0 for constants

        Equations
        Instances For
          @[simp]
          theorem Polynomial.nextCoeffUp_C_eq_zero {R : Type u} [Semiring R] (c : R) :
          Polynomial.nextCoeffUp (Polynomial.C c) = 0