# Documentation

Mathlib.Data.Polynomial.Degree.TrailingDegree

# Trailing degree of univariate polynomials #

## Main definitions #

• trailingDegree p: the multiplicity of X in the polynomial p
• natTrailingDegree: a variant of trailingDegree that takes values in the natural numbers
• trailingCoeff: the coefficient at index natTrailingDegree p

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

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

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 = ⊤.

Instances For
def Polynomial.natTrailingDegree {R : Type u} [] (p : ) :

natTrailingDegree p forces trailingDegree p to ℕ, by defining natTrailingDegree ⊤ = 0.

Instances For
def Polynomial.trailingCoeff {R : Type u} [] (p : ) :
R

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

Instances For
def Polynomial.TrailingMonic {R : Type u} [] (p : ) :

a polynomial is monic_at if its trailing coefficient is 1

Instances For
theorem Polynomial.TrailingMonic.def {R : Type u} [] {p : } :
instance Polynomial.TrailingMonic.decidable {R : Type u} [] {p : } :
@[simp]
theorem Polynomial.TrailingMonic.trailingCoeff {R : Type u} [] {p : } (hp : ) :
@[simp]
@[simp]
theorem Polynomial.trailingCoeff_zero {R : Type u} [] :
@[simp]
theorem Polynomial.trailingDegree_eq_top {R : Type u} [] {p : } :
p = 0
theorem Polynomial.trailingDegree_eq_natTrailingDegree {R : Type u} [] {p : } (hp : p 0) :
theorem Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq {R : Type u} [] {p : } {n : } (hp : p 0) :
theorem Polynomial.natTrailingDegree_eq_of_trailingDegree_eq {R : Type u} {S : Type v} [] {p : } [] {q : } :
theorem Polynomial.le_trailingDegree_of_ne_zero {R : Type u} {n : } [] {p : } (h : 0) :
theorem Polynomial.natTrailingDegree_le_of_ne_zero {R : Type u} {n : } [] {p : } (h : 0) :
theorem Polynomial.trailingDegree_le_trailingDegree {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.natTrailingDegree_le_of_trailingDegree_le {R : Type u} [] {p : } {n : } {hp : p 0} (H : ) :
theorem Polynomial.natTrailingDegree_le_natTrailingDegree {R : Type u} [] {p : } {q : } {hq : q 0} (hpq : ) :
@[simp]
theorem Polynomial.trailingDegree_monomial {R : Type u} {a : R} {n : } [] (ha : a 0) :
= n
theorem Polynomial.natTrailingDegree_monomial {R : Type u} {a : R} {n : } [] (ha : a 0) :
theorem Polynomial.natTrailingDegree_monomial_le {R : Type u} {a : R} {n : } [] :
theorem Polynomial.le_trailingDegree_monomial {R : Type u} {a : R} {n : } [] :
n
@[simp]
theorem Polynomial.trailingDegree_C {R : Type u} {a : R} [] (ha : a 0) :
Polynomial.trailingDegree (Polynomial.C a) = 0
theorem Polynomial.le_trailingDegree_C {R : Type u} {a : R} [] :
0 Polynomial.trailingDegree (Polynomial.C a)
@[simp]
theorem Polynomial.natTrailingDegree_C {R : Type u} [] (a : R) :
Polynomial.natTrailingDegree (Polynomial.C a) = 0
@[simp]
@[simp]
@[simp]
theorem Polynomial.trailingDegree_C_mul_X_pow {R : Type u} {a : 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} [] (n : ) (a : R) :
n Polynomial.trailingDegree (Polynomial.C a * Polynomial.X ^ n)
theorem Polynomial.coeff_eq_zero_of_trailingDegree_lt {R : Type u} {n : } [] {p : } (h : ) :
= 0
theorem Polynomial.coeff_eq_zero_of_lt_natTrailingDegree {R : Type u} [] {p : } {n : } (h : ) :
= 0
@[simp]
theorem Polynomial.coeff_natTrailingDegree_pred_eq_zero {R : Type u} [] {p : } {hp : } :
theorem Polynomial.le_trailingDegree_X_pow {R : Type u} [] (n : ) :
n Polynomial.trailingDegree (Polynomial.X ^ n)
@[simp]
theorem Polynomial.trailingCoeff_eq_zero {R : Type u} [] {p : } :
p = 0
theorem Polynomial.natTrailingDegree_eq_support_min' {R : Type u} [] {p : } (h : p 0) :
theorem Polynomial.le_natTrailingDegree {R : Type u} {n : } [] {p : } (hp : p 0) (hn : ∀ (m : ), m < n = 0) :
theorem Polynomial.natTrailingDegree_mul_X_pow {R : Type u} [] {p : } (hp : p 0) (n : ) :
Polynomial.natTrailingDegree (p * Polynomial.X ^ n) =
theorem Polynomial.le_trailingDegree_mul {R : Type u} [] {p : } {q : } :
theorem Polynomial.le_natTrailingDegree_mul {R : Type u} [] {p : } {q : } (h : p * q 0) :
theorem Polynomial.trailingDegree_mul' {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.natTrailingDegree_mul' {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.natTrailingDegree_mul {R : Type u} [] {p : } {q : } [] (hp : p 0) (hq : q 0) :
@[simp]
theorem Polynomial.trailingDegree_one {R : Type u} [] [] :
@[simp]
theorem Polynomial.trailingDegree_X {R : Type u} [] [] :
@[simp]
@[simp]
theorem Polynomial.trailingDegree_neg {R : Type u} [Ring R] (p : ) :
@[simp]
theorem Polynomial.natTrailingDegree_neg {R : Type u} [Ring R] (p : ) :
@[simp]
def Polynomial.nextCoeffUp {R : Type u} [] (p : ) :
R

The second-lowest coefficient, or 0 for constants

Instances For
@[simp]
theorem Polynomial.nextCoeffUp_C_eq_zero {R : Type u} [] (c : R) :
Polynomial.nextCoeffUp (Polynomial.C c) = 0
theorem Polynomial.ne_zero_of_trailingDegree_lt {R : Type u} [] {p : } {n : ℕ∞} (h : ) :
p 0