Documentation

Mathlib.Algebra.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

      natTrailingDegree p forces trailingDegree p to , by defining natTrailingDegree ⊤ = 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
                  @[simp]
                  theorem Polynomial.trailingDegree_monomial {R : Type u} {a : R} {n : } [Semiring R] (ha : a 0) :
                  theorem Polynomial.natTrailingDegree_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) :
                  @[simp]
                  @[simp]
                  theorem Polynomial.trailingDegree_C_mul_X_pow {R : Type u} {a : R} [Semiring R] (n : ) (ha : a 0) :
                  (C a * X ^ n).trailingDegree = n
                  theorem Polynomial.le_trailingDegree_C_mul_X_pow {R : Type u} [Semiring R] (n : ) (a : R) :
                  n (C a * X ^ n).trailingDegree
                  @[simp]
                  theorem Polynomial.le_natTrailingDegree {R : Type u} {n : } [Semiring R] {p : Polynomial R} (hp : p 0) (hn : m < n, p.coeff m = 0) :
                  @[simp]
                  @[simp]
                  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) :