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} [Semiring R] (p : Polynomial R) : ℕ∞

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

theorem Polynomial.trailingDegree_lt_wf {R : Type u} [Semiring R] : WellFounded fun (p q : Polynomial R) => p.trailingDegree < q.trailingDegree

def Polynomial.natTrailingDegree {R : Type u} [Semiring R] (p : Polynomial R) : ℕ

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

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

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

def Polynomial.TrailingMonic {R : Type u} [Semiring R] (p : Polynomial R) : Prop

a polynomial is monic_at if its trailing coefficient is 1

theorem Polynomial.TrailingMonic.def {R : Type u} [Semiring R] {p : Polynomial R} : p.TrailingMonic ↔ p.trailingCoeff = 1

@[implicit_reducible]

instance Polynomial.TrailingMonic.decidable {R : Type u} [Semiring R] {p : Polynomial R} [DecidableEq R] : Decidable p.TrailingMonic

@[simp]

theorem Polynomial.TrailingMonic.trailingCoeff {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.TrailingMonic) : p.trailingCoeff = 1

@[simp]

theorem Polynomial.trailingDegree_zero {R : Type u} [Semiring R] : trailingDegree 0 = ⊤

@[simp]

theorem Polynomial.trailingCoeff_zero {R : Type u} [Semiring R] : trailingCoeff 0 = 0

@[simp]

theorem Polynomial.natTrailingDegree_zero {R : Type u} [Semiring R] : natTrailingDegree 0 = 0

@[simp]

theorem Polynomial.trailingDegree_eq_top {R : Type u} [Semiring R] {p : Polynomial R} : p.trailingDegree = ⊤ ↔ p = 0

theorem Polynomial.trailingDegree_eq_natTrailingDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.trailingDegree = ↑p.natTrailingDegree

theorem Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hp : p ≠ 0) : p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

theorem Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq_of_pos {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : n ≠ 0) : p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

theorem Polynomial.natTrailingDegree_eq_of_trailingDegree_eq_some {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.trailingDegree = ↑n) : p.natTrailingDegree = n

@[simp]

theorem Polynomial.natTrailingDegree_le_trailingDegree {R : Type u} [Semiring R] {p : Polynomial R} : ↑p.natTrailingDegree ≤ p.trailingDegree

theorem Polynomial.natTrailingDegree_eq_of_trailingDegree_eq {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {q : Polynomial S} (h : p.trailingDegree = q.trailingDegree) : p.natTrailingDegree = q.natTrailingDegree

theorem Polynomial.trailingDegree_le_of_ne_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) : p.trailingDegree ≤ ↑n

theorem Polynomial.natTrailingDegree_le_of_ne_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) : p.natTrailingDegree ≤ n

@[simp]

theorem Polynomial.coeff_natTrailingDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff p.natTrailingDegree = 0 ↔ p = 0

theorem Polynomial.coeff_natTrailingDegree_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff p.natTrailingDegree ≠ 0 ↔ p ≠ 0

@[simp]

theorem Polynomial.trailingDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.trailingDegree = 0 ↔ p.coeff 0 ≠ 0

@[simp]

theorem Polynomial.natTrailingDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0

theorem Polynomial.natTrailingDegree_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.natTrailingDegree ≠ 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0

theorem Polynomial.trailingDegree_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.trailingDegree ≠ 0 ↔ p.coeff 0 = 0

@[simp]

theorem Polynomial.trailingDegree_le_trailingDegree {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.coeff p.natTrailingDegree ≠ 0) : q.trailingDegree ≤ p.trailingDegree

theorem Polynomial.trailingCoeff_eq_coeff_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.coeff 0 ≠ 0) : p.trailingCoeff = p.coeff 0

theorem Polynomial.trailingDegree_ne_of_natTrailingDegree_ne {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.natTrailingDegree ≠ n → p.trailingDegree ≠ ↑n

theorem Polynomial.natTrailingDegree_le_of_trailingDegree_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} {hp : p ≠ 0} (H : ↑n ≤ p.trailingDegree) : n ≤ p.natTrailingDegree

theorem Polynomial.natTrailingDegree_le_natTrailingDegree {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q ≠ 0) (hpq : p.trailingDegree ≤ q.trailingDegree) : p.natTrailingDegree ≤ q.natTrailingDegree

@[simp]

theorem Polynomial.trailingDegree_monomial {R : Type u} {a : R} {n : ℕ} [Semiring R] (ha : a ≠ 0) : ((monomial n) a).trailingDegree = ↑n

theorem Polynomial.natTrailingDegree_monomial {R : Type u} {a : R} {n : ℕ} [Semiring R] (ha : a ≠ 0) : ((monomial n) a).natTrailingDegree = n

theorem Polynomial.natTrailingDegree_monomial_le {R : Type u} {a : R} {n : ℕ} [Semiring R] : ((monomial n) a).natTrailingDegree ≤ n

theorem Polynomial.le_trailingDegree_monomial {R : Type u} {a : R} {n : ℕ} [Semiring R] : ↑n ≤ ((monomial n) a).trailingDegree

@[simp]

theorem Polynomial.trailingDegree_C {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) : (C a).trailingDegree = 0

theorem Polynomial.le_trailingDegree_C {R : Type u} {a : R} [Semiring R] : 0 ≤ (C a).trailingDegree

theorem Polynomial.trailingDegree_one_le {R : Type u} [Semiring R] : 0 ≤ trailingDegree 1

@[simp]

theorem Polynomial.natTrailingDegree_C {R : Type u} [Semiring R] (a : R) : (C a).natTrailingDegree = 0

@[simp]

theorem Polynomial.natTrailingDegree_one {R : Type u} [Semiring R] : natTrailingDegree 1 = 0

@[simp]

theorem Polynomial.natTrailingDegree_natCast {R : Type u} [Semiring R] (n : ℕ) : (↑n).natTrailingDegree = 0

@[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

theorem Polynomial.coeff_eq_zero_of_lt_trailingDegree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : ↑n < p.trailingDegree) : p.coeff n = 0

theorem Polynomial.coeff_eq_zero_of_lt_natTrailingDegree {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : n < p.natTrailingDegree) : p.coeff n = 0

@[simp]

theorem Polynomial.coeff_natTrailingDegree_pred_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {hp : 0 < ↑p.natTrailingDegree} : p.coeff (p.natTrailingDegree - 1) = 0

theorem Polynomial.le_trailingDegree_X_pow {R : Type u} [Semiring R] (n : ℕ) : ↑n ≤ (X ^ n).trailingDegree

theorem Polynomial.le_trailingDegree_X {R : Type u} [Semiring R] : 1 ≤ X.trailingDegree

theorem Polynomial.natTrailingDegree_X_le {R : Type u} [Semiring R] : X.natTrailingDegree ≤ 1

@[simp]

theorem Polynomial.trailingCoeff_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.trailingCoeff = 0 ↔ p = 0

theorem Polynomial.trailingCoeff_nonzero_iff_nonzero {R : Type u} [Semiring R] {p : Polynomial R} : p.trailingCoeff ≠ 0 ↔ p ≠ 0

theorem Polynomial.natTrailingDegree_mem_support_of_nonzero {R : Type u} [Semiring R] {p : Polynomial R} : p ≠ 0 → p.natTrailingDegree ∈ p.support

theorem Polynomial.natTrailingDegree_le_of_mem_supp {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → p.natTrailingDegree ≤ a

theorem Polynomial.natTrailingDegree_eq_support_min' {R : Type u} [Semiring R] {p : Polynomial R} (h : p ≠ 0) : p.natTrailingDegree = p.support.min' ⋯

theorem Polynomial.le_natTrailingDegree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (hn : ∀ m < n, p.coeff m = 0) : n ≤ p.natTrailingDegree

theorem Polynomial.natTrailingDegree_le_natDegree {R : Type u} [Semiring R] (p : Polynomial R) : p.natTrailingDegree ≤ p.natDegree

theorem Polynomial.natTrailingDegree_mul_X_pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (n : ℕ) : (p * X ^ n).natTrailingDegree = p.natTrailingDegree + n

theorem Polynomial.le_trailingDegree_mul {R : Type u} [Semiring R] {p q : Polynomial R} : p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

theorem Polynomial.le_natTrailingDegree_mul {R : Type u} [Semiring R] {p q : Polynomial R} (h : p * q ≠ 0) : p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

theorem Polynomial.coeff_mul_natTrailingDegree_add_natTrailingDegree {R : Type u} [Semiring R] {p q : Polynomial R} : (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff

theorem Polynomial.trailingDegree_mul' {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.trailingCoeff * q.trailingCoeff ≠ 0) : (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

theorem Polynomial.natTrailingDegree_mul' {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.trailingCoeff * q.trailingCoeff ≠ 0) : (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

theorem Polynomial.natTrailingDegree_mul {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (hp : p ≠ 0) (hq : q ≠ 0) : (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

@[simp]

theorem Polynomial.trailingDegree_one {R : Type u} [Semiring R] [Nontrivial R] : trailingDegree 1 = 0

@[simp]

theorem Polynomial.trailingDegree_X {R : Type u} [Semiring R] [Nontrivial R] : X.trailingDegree = 1

@[simp]

theorem Polynomial.natTrailingDegree_X {R : Type u} [Semiring R] [Nontrivial R] : X.natTrailingDegree = 1

@[simp]

theorem Polynomial.trailingDegree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (X ^ n).trailingDegree = ↑n

@[simp]

theorem Polynomial.natTrailingDegree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (X ^ n).natTrailingDegree = n

@[simp]

theorem Polynomial.trailingDegree_neg {R : Type u} [Ring R] (p : Polynomial R) : (-p).trailingDegree = p.trailingDegree

@[simp]

theorem Polynomial.natTrailingDegree_neg {R : Type u} [Ring R] (p : Polynomial R) : (-p).natTrailingDegree = p.natTrailingDegree

@[simp]

theorem Polynomial.natTrailingDegree_intCast {R : Type u} [Ring R] (n : ℤ) : (↑n).natTrailingDegree = 0

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

The second-lowest coefficient, or 0 for constants

@[simp]

theorem Polynomial.nextCoeffUp_zero {R : Type u} [Semiring R] : nextCoeffUp 0 = 0

@[simp]

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

theorem Polynomial.nextCoeffUp_of_constantCoeff_eq_zero {R : Type u} [Semiring R] (p : Polynomial R) (hp : p.coeff 0 = 0) : p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

theorem Polynomial.coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.trailingDegree < q.trailingDegree) : q.coeff p.natTrailingDegree = 0

theorem Polynomial.ne_zero_of_trailingDegree_lt {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ∞} (h : p.trailingDegree < n) : p ≠ 0

theorem Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : constantCoeff p ≠ 0) : p.natTrailingDegree = 0

theorem Polynomial.Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree {R : Type u} [Semiring R] {p : Polynomial R} (h₁ : p.Monic) : p = X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree

theorem Polynomial.Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (h₁ : p.Monic) : p = X ^ p.natDegree ↔ p.natTrailingDegree = p.natDegree