mathlib3 documentation

data.polynomial.degree.trailing_degree

Trailing degree of univariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Converts most results about degree, nat_degree and leading_coeff to results about the bottom end of a polynomial

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

Equations

nat_trailing_degree p forces trailing_degree p to , by defining nat_trailing_degree ⊤ = 0.

Equations
def polynomial.trailing_coeff {R : Type u} [semiring R] (p : polynomial R) :
R

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

Equations
def polynomial.trailing_monic {R : Type u} [semiring R] (p : polynomial R) :
Prop

a polynomial is monic_at if its trailing coefficient is 1

Equations
Instances for polynomial.trailing_monic
@[protected, instance]
Equations
@[simp]
@[simp]
theorem polynomial.trailing_degree_monomial {R : Type u} {a : R} {n : } [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.trailing_degree_C {R : Type u} {a : R} [semiring R] (ha : a 0) :
@[simp]
@[simp]
theorem polynomial.le_nat_trailing_degree {R : Type u} {n : } [semiring R] {p : polynomial R} (hp : p 0) (hn : (m : ), m < n p.coeff m = 0) :
def polynomial.next_coeff_up {R : Type u} [semiring R] (p : polynomial R) :
R

The second-lowest coefficient, or 0 for constants

Equations