Documentation

Mathlib.Algebra.Polynomial.Degree.Definitions

Degree of univariate polynomials #

Main definitions #

Main results #

degree p is the degree of the polynomial p, i.e. the largest X-exponent in p. degree p = some n when p ≠ 0 and n is the highest power of X that appears in p, otherwise degree 0 = ⊥.

Equations
Instances For

    natDegree p forces degree p to ℕ, by defining natDegree 0 = 0.

    Equations
    Instances For
      def Polynomial.leadingCoeff {R : Type u} [Semiring R] (p : Polynomial R) :
      R

      leadingCoeff p gives the coefficient of the highest power of X in p

      Equations
      Instances For
        def Polynomial.Monic {R : Type u} [Semiring R] (p : Polynomial R) :

        a polynomial is Monic if its leading coefficient is 1

        Equations
        Instances For
          @[simp]
          @[simp]
          @[simp]
          @[simp]

          Alias of the forward direction of Polynomial.natDegree_le_iff_degree_le.

          Alias of the reverse direction of Polynomial.natDegree_le_iff_degree_le.

          @[simp]
          theorem Polynomial.degree_C {R : Type u} {a : R} [Semiring R] (ha : a 0) :
          (C a).degree = 0
          theorem Polynomial.degree_C_le {R : Type u} {a : R} [Semiring R] :
          theorem Polynomial.degree_C_lt {R : Type u} {a : R} [Semiring R] :
          (C a).degree < 1
          @[simp]
          theorem Polynomial.natDegree_C {R : Type u} [Semiring R] (a : R) :
          @[simp]
          @[simp]
          theorem Polynomial.degree_monomial {R : Type u} {a : R} [Semiring R] (n : ) (ha : a 0) :
          ((monomial n) a).degree = n
          @[simp]
          theorem Polynomial.degree_C_mul_X_pow {R : Type u} {a : R} [Semiring R] (n : ) (ha : a 0) :
          (C a * X ^ n).degree = n
          theorem Polynomial.degree_C_mul_X {R : Type u} {a : R} [Semiring R] (ha : a 0) :
          (C a * X).degree = 1
          theorem Polynomial.degree_monomial_le {R : Type u} [Semiring R] (n : ) (a : R) :
          ((monomial n) a).degree n
          theorem Polynomial.degree_C_mul_X_pow_le {R : Type u} [Semiring R] (n : ) (a : R) :
          (C a * X ^ n).degree n
          theorem Polynomial.degree_C_mul_X_le {R : Type u} [Semiring R] (a : R) :
          (C a * X).degree 1
          @[simp]
          theorem Polynomial.natDegree_C_mul_X_pow {R : Type u} [Semiring R] (n : ) (a : R) (ha : a 0) :
          (C a * X ^ n).natDegree = n
          @[simp]
          theorem Polynomial.natDegree_C_mul_X {R : Type u} [Semiring R] (a : R) (ha : a 0) :
          @[simp]
          theorem Polynomial.natDegree_monomial {R : Type u} [Semiring R] [DecidableEq R] (i : ) (r : R) :
          theorem Polynomial.natDegree_monomial_eq {R : Type u} [Semiring R] (i : ) {r : R} (r0 : r 0) :
          theorem Polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : } [Semiring R] {p : Polynomial R} (hn : p.degree = n) :
          theorem Polynomial.degree_X_pow_le {R : Type u} [Semiring R] (n : ) :
          (X ^ n).degree n
          @[simp]
          theorem Polynomial.degree_one {R : Type u} [Semiring R] [Nontrivial R] :
          degree 1 = 0
          @[simp]
          theorem Polynomial.degree_X {R : Type u} [Semiring R] [Nontrivial R] :
          @[simp]
          @[simp]
          theorem Polynomial.degree_neg {R : Type u} [Ring R] (p : Polynomial R) :
          theorem Polynomial.degree_neg_le_of_le {R : Type u} [Ring R] {a : WithBot } {p : Polynomial R} (hp : p.degree a) :
          @[simp]
          @[simp]
          def Polynomial.nextCoeff {R : Type u} [Semiring R] (p : Polynomial R) :
          R

          The second-highest coefficient, or 0 for constants

          Equations
          Instances For
            @[simp]
            theorem Polynomial.nextCoeff_C_eq_zero {R : Type u} [Semiring R] (c : R) :
            theorem Polynomial.degree_add_le_of_degree_le {R : Type u} [Semiring R] {p q : Polynomial R} {n : } (hp : p.degree n) (hq : q.degree n) :
            (p + q).degree n
            theorem Polynomial.degree_add_le_of_le {R : Type u} [Semiring R] {p q : Polynomial R} {a b : WithBot } (hp : p.degree a) (hq : q.degree b) :
            theorem Polynomial.natDegree_C_mul_X_pow_le {R : Type u} [Semiring R] (a : R) (n : ) :
            (C a * X ^ n).natDegree n
            theorem Polynomial.degree_update_le {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (a : R) :
            theorem Polynomial.degree_sum_le {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ιPolynomial R) :
            (∑ is, f i).degree s.sup fun (b : ι) => (f b).degree
            theorem Polynomial.degree_mul_le_of_le {R : Type u} [Semiring R] {p q : Polynomial R} {a b : WithBot } (hp : p.degree a) (hq : q.degree b) :
            @[simp]
            theorem Polynomial.leadingCoeff_monomial {R : Type u} [Semiring R] (a : R) (n : ) :
            theorem Polynomial.leadingCoeff_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ) :
            (C a * X ^ n).leadingCoeff = a
            @[simp]
            theorem Polynomial.leadingCoeff_C {R : Type u} [Semiring R] (a : R) :
            @[simp]
            theorem Polynomial.monic_X_pow {R : Type u} [Semiring R] (n : ) :
            @[simp]
            theorem Polynomial.monic_X {R : Type u} [Semiring R] :
            @[simp]
            theorem Polynomial.monic_one {R : Type u} [Semiring R] :
            theorem Polynomial.Monic.ne_zero {R : Type u_2} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p.Monic) :
            theorem Polynomial.Monic.ne_zero_of_ne {R : Type u} [Semiring R] (h : 0 1) {p : Polynomial R} (hp : p.Monic) :
            theorem Polynomial.Monic.ne_zero_of_polynomial_ne {R : Type u} [Semiring R] {p q r : Polynomial R} (hp : p.Monic) (hne : q r) :
            theorem Polynomial.natDegree_mul_le_of_le {R : Type u} {n m : } [Semiring R] {p q : Polynomial R} (hp : p.natDegree m) (hg : q.natDegree n) :
            theorem Polynomial.degree_le_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : WithBot ) :
            f.degree n ∀ (m : ), n < mf.coeff m = 0
            theorem Polynomial.degree_lt_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : ) :
            f.degree < n ∀ (m : ), n mf.coeff m = 0
            @[simp]
            theorem Polynomial.degree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ) :
            (X ^ n).degree = n
            @[simp]
            theorem Polynomial.natDegree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ) :
            theorem Polynomial.degree_sub_le_of_le {R : Type u} [Ring R] {p q : Polynomial R} {a b : WithBot } (hp : p.degree a) (hq : q.degree b) :
            theorem Polynomial.natDegree_sub_le_of_le {R : Type u} {n m : } [Ring R] {p q : Polynomial R} (hp : p.natDegree m) (hq : q.natDegree n) :
            theorem Polynomial.degree_sub_lt {R : Type u} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hp0 : p 0) (hlc : p.leadingCoeff = q.leadingCoeff) :
            theorem Polynomial.degree_X_sub_C_le {R : Type u} [Ring R] (r : R) :
            (X - C r).degree 1
            theorem Polynomial.natDegree_X_sub_C_le {R : Type u} [Ring R] (r : R) :