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.trailingDegree p < Polynomial.trailingDegree q

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} : Polynomial.TrailingMonic p ↔ Polynomial.trailingCoeff p = 1

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.trailingDegree_C_mul_X_pow {R : Type u} {a : R} [Semiring 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} [Semiring R] (n : ℕ) (a : R) : ↑n ≤ Polynomial.trailingDegree (↑Polynomial.C a * Polynomial.X ^ n)

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

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.natTrailingDegree_int_cast {R : Type u} [Ring R] (n : ℤ) : Polynomial.natTrailingDegree ↑n = 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_C_eq_zero {R : Type u} [Semiring R] (c : R) : Polynomial.nextCoeffUp (↑Polynomial.C c) = 0

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

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

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