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

Equations

• Polynomial.trailingDegree p = Finset.min (Polynomial.support p)

theorem Polynomial.trailingDegree_lt_wf {R : Type u} [Semiring R] : WellFounded fun (p q : Polynomial R) => 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.

Equations

• Polynomial.natTrailingDegree p = Option.getD (Polynomial.trailingDegree p) 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

Equations

• Polynomial.trailingCoeff p = Polynomial.coeff p (Polynomial.natTrailingDegree p)

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

a polynomial is monic_at if its trailing coefficient is 1

Equations

• Polynomial.TrailingMonic p = (Polynomial.trailingCoeff p = 1)

theorem Polynomial.TrailingMonic.definition {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} [DecidableEq R] : Decidable (Polynomial.TrailingMonic p)

Equations

• Polynomial.TrailingMonic.decidable = inferInstanceAs (Decidable (Polynomial.trailingCoeff p = 1))

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

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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_lt_trailingDegree {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) ⋯

theorem Polynomial.le_natTrailingDegree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (hn : ∀ 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_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : Polynomial.trailingDegree (Polynomial.X ^ n) = ↑n

@[simp]

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

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

Equations

• Polynomial.nextCoeffUp p = if Polynomial.natTrailingDegree p = 0 then 0 else Polynomial.coeff p (Polynomial.natTrailingDegree p + 1)

@[simp]

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

@[simp]

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

theorem Polynomial.nextCoeffUp_of_constantCoeff_eq_zero {R : Type u} [Semiring R] (p : Polynomial R) (hp : Polynomial.coeff p 0 = 0) : 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

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

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