# mathlibdocumentation

data.polynomial.degree.trailing_degree

# Trailing degree of univariate polynomials #

## Main definitions #

• trailing_degree p: the multiplicity of X in the polynomial p
• nat_trailing_degree: a variant of trailing_degree that takes values in the natural numbers
• trailing_coeff: the coefficient at index nat_trailing_degree p

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

noncomputable def polynomial.trailing_degree {R : Type u} [semiring R] (p : polynomial R) :

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
theorem polynomial.trailing_degree_lt_wf {R : Type u} [semiring R] :
well_founded (λ (p q : ,
noncomputable def polynomial.nat_trailing_degree {R : Type u} [semiring R] (p : polynomial R) :

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

Equations
noncomputable 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
theorem polynomial.trailing_monic.def {R : Type u} [semiring R] {p : polynomial R} :
@[protected, instance]
noncomputable def polynomial.trailing_monic.decidable {R : Type u} [semiring R] {p : polynomial R} [decidable_eq R] :
Equations
@[simp]
theorem polynomial.trailing_monic.trailing_coeff {R : Type u} [semiring R] {p : polynomial R} (hp : p.trailing_monic) :
@[simp]
theorem polynomial.trailing_degree_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.trailing_coeff_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.nat_trailing_degree_zero {R : Type u} [semiring R] :
theorem polynomial.trailing_degree_eq_top {R : Type u} [semiring R] {p : polynomial R} :
p = 0
theorem polynomial.trailing_degree_eq_nat_trailing_degree {R : Type u} [semiring R] {p : polynomial R} (hp : p 0) :
theorem polynomial.trailing_degree_eq_iff_nat_trailing_degree_eq {R : Type u} [semiring R] {p : polynomial R} {n : } (hp : p 0) :
@[simp]
theorem polynomial.le_trailing_degree_of_ne_zero {R : Type u} {n : } [semiring R] {p : polynomial R} (h : p.coeff n 0) :
theorem polynomial.nat_trailing_degree_le_of_ne_zero {R : Type u} {n : } [semiring R] {p : polynomial R} (h : p.coeff n 0) :
theorem polynomial.trailing_degree_le_trailing_degree {R : Type u} [semiring R] {p q : polynomial R} (h : 0) :
theorem polynomial.nat_trailing_degree_le_of_trailing_degree_le {R : Type u} [semiring R] {p : polynomial R} {n : } {hp : p 0} (H : n p.trailing_degree) :
@[simp]
theorem polynomial.trailing_degree_monomial {R : Type u} {a : R} {n : } [semiring R] (ha : a 0) :
theorem polynomial.nat_trailing_degree_monomial {R : Type u} {a : R} {n : } [semiring R] (ha : a 0) :
= n
theorem polynomial.nat_trailing_degree_monomial_le {R : Type u} {a : R} {n : } [semiring R] :
n
theorem polynomial.le_trailing_degree_monomial {R : Type u} {a : R} {n : } [semiring R] :
@[simp]
theorem polynomial.trailing_degree_C {R : Type u} {a : R} [semiring R] (ha : a 0) :
theorem polynomial.le_trailing_degree_C {R : Type u} {a : R} [semiring R] :
theorem polynomial.trailing_degree_one_le {R : Type u} [semiring R] :
@[simp]
theorem polynomial.nat_trailing_degree_C {R : Type u} [semiring R] (a : R) :
@[simp]
theorem polynomial.nat_trailing_degree_one {R : Type u} [semiring R] :
@[simp]
theorem polynomial.nat_trailing_degree_nat_cast {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.trailing_degree_C_mul_X_pow {R : Type u} {a : R} [semiring R] (n : ) (ha : a 0) :
= n
theorem polynomial.le_trailing_degree_C_mul_X_pow {R : Type u} [semiring R] (n : ) (a : R) :
theorem polynomial.coeff_eq_zero_of_trailing_degree_lt {R : Type u} {n : } [semiring R] {p : polynomial R} (h : n < p.trailing_degree) :
p.coeff n = 0
theorem polynomial.le_trailing_degree_X_pow {R : Type u} [semiring R] (n : ) :
theorem polynomial.le_trailing_degree_X {R : Type u} [semiring R] :
@[simp]
theorem polynomial.trailing_coeff_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p = 0
theorem polynomial.nat_trailing_degree_le_of_mem_supp {R : Type u} [semiring R] {p : polynomial R} (a : ) :
a p.support
theorem polynomial.nat_trailing_degree_eq_support_min' {R : Type u} [semiring R] {p : polynomial R} (h : p 0) :
theorem polynomial.le_nat_trailing_degree {R : Type u} {n : } [semiring R] {p : polynomial R} (hp : p 0) (hn : ∀ (m : ), m < np.coeff m = 0) :
theorem polynomial.nat_trailing_degree_mul_X_pow {R : Type u} [semiring R] {p : polynomial R} (hp : p 0) (n : ) :
theorem polynomial.le_trailing_degree_mul {R : Type u} [semiring R] {p q : polynomial R} :
theorem polynomial.le_nat_trailing_degree_mul {R : Type u} [semiring R] {p q : polynomial R} (h : p * q 0) :
theorem polynomial.trailing_degree_mul' {R : Type u} [semiring R] {p q : polynomial R} (h : 0) :
theorem polynomial.nat_trailing_degree_mul' {R : Type u} [semiring R] {p q : polynomial R} (h : 0) :
theorem polynomial.nat_trailing_degree_mul {R : Type u} [semiring R] {p q : polynomial R} (hp : p 0) (hq : q 0) :
@[simp]
theorem polynomial.trailing_degree_one {R : Type u} [semiring R] [nontrivial R] :
@[simp]
theorem polynomial.trailing_degree_X {R : Type u} [semiring R] [nontrivial R] :
@[simp]
theorem polynomial.nat_trailing_degree_X {R : Type u} [semiring R] [nontrivial R] :
@[simp]
theorem polynomial.trailing_degree_neg {R : Type u} [ring R] (p : polynomial R) :
@[simp]
theorem polynomial.nat_trailing_degree_neg {R : Type u} [ring R] (p : polynomial R) :
@[simp]
theorem polynomial.nat_trailing_degree_int_cast {R : Type u} [ring R] (n : ) :
noncomputable def polynomial.next_coeff_up {R : Type u} [semiring R] (p : polynomial R) :
R

The second-lowest coefficient, or 0 for constants

Equations
@[simp]
theorem polynomial.next_coeff_up_C_eq_zero {R : Type u} [semiring R] (c : R) :
theorem polynomial.ne_zero_of_trailing_degree_lt {R : Type u} [semiring R] {p : polynomial R} {n : ℕ∞} (h : p.trailing_degree < n) :
p 0