Documentation

Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Trailing degree of univariate polynomials #

Main definitions #

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

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

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

    Equations
    • p.natTrailingDegree = p.trailingDegree.toNat
    Instances For

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

      Equations
      • p.trailingCoeff = p.coeff p.natTrailingDegree
      Instances For

        a polynomial is monic_at if its trailing coefficient is 1

        Equations
        • p.TrailingMonic = (p.trailingCoeff = 1)
        Instances For
          theorem Polynomial.TrailingMonic.def {R : Type u} [Semiring R] {p : Polynomial R} :
          p.TrailingMonic p.trailingCoeff = 1
          instance Polynomial.TrailingMonic.decidable {R : Type u} [Semiring R] {p : Polynomial R} [DecidableEq R] :
          Decidable p.TrailingMonic
          Equations
          @[simp]
          theorem Polynomial.TrailingMonic.trailingCoeff {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.TrailingMonic) :
          p.trailingCoeff = 1
          @[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 : Polynomial R} {q : Polynomial R} (h : q.coeff p.natTrailingDegree 0) :
          q.trailingDegree p.trailingDegree
          theorem Polynomial.trailingDegree_ne_of_natTrailingDegree_ne {R : Type u} [Semiring R] {p : Polynomial R} {n : } :
          p.natTrailingDegree np.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 : Polynomial R} {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) :
          ((Polynomial.monomial n) a).trailingDegree = n
          theorem Polynomial.natTrailingDegree_monomial {R : Type u} {a : R} {n : } [Semiring R] (ha : a 0) :
          ((Polynomial.monomial n) a).natTrailingDegree = n
          theorem Polynomial.natTrailingDegree_monomial_le {R : Type u} {a : R} {n : } [Semiring R] :
          ((Polynomial.monomial n) a).natTrailingDegree n
          theorem Polynomial.le_trailingDegree_monomial {R : Type u} {a : R} {n : } [Semiring R] :
          n ((Polynomial.monomial n) a).trailingDegree
          @[simp]
          theorem Polynomial.trailingDegree_C {R : Type u} {a : R} [Semiring R] (ha : a 0) :
          (Polynomial.C a).trailingDegree = 0
          theorem Polynomial.le_trailingDegree_C {R : Type u} {a : R} [Semiring R] :
          0 (Polynomial.C a).trailingDegree
          @[simp]
          theorem Polynomial.natTrailingDegree_C {R : Type u} [Semiring R] (a : R) :
          (Polynomial.C a).natTrailingDegree = 0
          @[simp]
          theorem Polynomial.natTrailingDegree_natCast {R : Type u} [Semiring R] (n : ) :
          (n).natTrailingDegree = 0
          @[deprecated Polynomial.natTrailingDegree_natCast]
          theorem Polynomial.natTrailingDegree_nat_cast {R : Type u} [Semiring R] (n : ) :
          (n).natTrailingDegree = 0

          Alias of Polynomial.natTrailingDegree_natCast.

          @[simp]
          theorem Polynomial.trailingDegree_C_mul_X_pow {R : Type u} {a : R} [Semiring R] (n : ) (ha : a 0) :
          (Polynomial.C a * Polynomial.X ^ n).trailingDegree = n
          theorem Polynomial.le_trailingDegree_C_mul_X_pow {R : Type u} [Semiring R] (n : ) (a : R) :
          n (Polynomial.C a * Polynomial.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 (Polynomial.X ^ n).trailingDegree
          theorem Polynomial.le_trailingDegree_X {R : Type u} [Semiring R] :
          1 Polynomial.X.trailingDegree
          theorem Polynomial.natTrailingDegree_X_le {R : Type u} [Semiring R] :
          Polynomial.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 0p.natTrailingDegree p.support
          theorem Polynomial.natTrailingDegree_le_of_mem_supp {R : Type u} [Semiring R] {p : Polynomial R} (a : ) :
          a p.supportp.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 * Polynomial.X ^ n).natTrailingDegree = p.natTrailingDegree + n
          theorem Polynomial.le_trailingDegree_mul {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
          p.trailingDegree + q.trailingDegree (p * q).trailingDegree
          theorem Polynomial.le_natTrailingDegree_mul {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {q : Polynomial R} :
          (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff
          theorem Polynomial.trailingDegree_mul' {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} [NoZeroDivisors R] (hp : p 0) (hq : q 0) :
          (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
          @[simp]
          theorem Polynomial.trailingDegree_X {R : Type u} [Semiring R] [Nontrivial R] :
          Polynomial.X.trailingDegree = 1
          @[simp]
          theorem Polynomial.natTrailingDegree_X {R : Type u} [Semiring R] [Nontrivial R] :
          Polynomial.X.natTrailingDegree = 1
          @[simp]
          theorem Polynomial.trailingDegree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ) :
          (Polynomial.X ^ n).trailingDegree = n
          @[simp]
          theorem Polynomial.natTrailingDegree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ) :
          (Polynomial.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
          @[deprecated Polynomial.natTrailingDegree_intCast]
          theorem Polynomial.natTrailingDegree_int_cast {R : Type u} [Ring R] (n : ) :
          (n).natTrailingDegree = 0

          Alias of Polynomial.natTrailingDegree_intCast.

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

          The second-lowest coefficient, or 0 for constants

          Equations
          • p.nextCoeffUp = if p.natTrailingDegree = 0 then 0 else p.coeff (p.natTrailingDegree + 1)
          Instances For
            @[simp]
            theorem Polynomial.nextCoeffUp_C_eq_zero {R : Type u} [Semiring R] (c : R) :
            (Polynomial.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 : Polynomial R} {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 : Polynomial.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 = Polynomial.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 = Polynomial.X ^ p.natDegree p.natTrailingDegree = p.natDegree
            @[deprecated Polynomial.Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]
            theorem Polynomial.Monic.eq_X_pow_of_natTrailingDegree_eq_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (h₁ : p.Monic) :
            p.natTrailingDegree = p.natDegreep = Polynomial.X ^ p.natDegree

            Alias of the reverse direction of Polynomial.Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree.