# Degree of univariate polynomials #

## Main definitions #

- `Polynomial.degree`: the degree of a polynomial, where `0` has degree `⊥`
- `Polynomial.natDegree`: the degree of a polynomial, where `0` has degree `0`
- `Polynomial.leadingCoeff`: the leading coefficient of a polynomial
- `Polynomial.Monic`: a polynomial is monic if its leading coefficient is 0
- `Polynomial.nextCoeff`: the next coefficient after the leading coefficient

## Main results #

- `Polynomial.degree_eq_natDegree`: the degree and natDegree coincide for nonzero polynomials

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

`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

- p.degree = p.support.max

Instances For

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

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

Equations

- p.natDegree = WithBot.unbotD 0 p.degree

Instances For

source
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

- p.leadingCoeff = p.coeff p.natDegree

Instances For

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

a polynomial is `Monic` if its leading coefficient is 1

Equations

- p.Monic = (p.leadingCoeff = 1)

Instances For

source
theorem Polynomial.Monic.def {R : Type u} [Semiring R] {p : Polynomial R} :
p.Monic ↔ p.leadingCoeff = 1
source
instance Polynomial.Monic.decidable {R : Type u} [Semiring R] {p : Polynomial R} [DecidableEq R] :
Decidable p.Monic
Equations

- Polynomial.Monic.decidable = id inferInstance

source
@[simp]
theorem Polynomial.Monic.leadingCoeff {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) :
p.leadingCoeff = 1
source
theorem Polynomial.Monic.coeff_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) :
p.coeff p.natDegree = 1
source
@[simp]
theorem Polynomial.degree_zero {R : Type u} [Semiring R] :
degree 0 = ⊥
source
@[simp]
theorem Polynomial.natDegree_zero {R : Type u} [Semiring R] :
natDegree 0 = 0
source
@[simp]
theorem Polynomial.coeff_natDegree {R : Type u} [Semiring R] {p : Polynomial R} :
p.coeff p.natDegree = p.leadingCoeff
source
@[simp]
theorem Polynomial.degree_eq_bot {R : Type u} [Semiring R] {p : Polynomial R} :
p.degree = ⊥ ↔ p = 0
source
theorem Polynomial.degree_ne_bot {R : Type u} [Semiring R] {p : Polynomial R} :
p.degree ≠ ⊥ ↔ p ≠ 0
source
theorem Polynomial.degree_eq_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) :
p.degree = ↑p.natDegree
source
theorem Polynomial.degree_eq_iff_natDegree_eq {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hp : p ≠ 0) :
p.degree = ↑n ↔ p.natDegree = n
source
theorem Polynomial.degree_eq_iff_natDegree_eq_of_pos {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : 0 < n) :
p.degree = ↑n ↔ p.natDegree = n
source
theorem Polynomial.natDegree_eq_of_degree_eq_some {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.degree = ↑n) :
p.natDegree = n
source
theorem Polynomial.degree_ne_of_natDegree_ne {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} :
p.natDegree ≠ n → p.degree ≠ ↑n
source
@[simp]
theorem Polynomial.degree_le_natDegree {R : Type u} [Semiring R] {p : Polynomial R} :
p.degree ≤ ↑p.natDegree
source
theorem Polynomial.natDegree_eq_of_degree_eq {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {q : Polynomial S} (h : p.degree = q.degree) :
p.natDegree = q.natDegree
source
theorem Polynomial.le_degree_of_ne_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) :
↑n ≤ p.degree
source
theorem Polynomial.degree_mono {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : Polynomial R} {g : Polynomial S} (h : f.support ⊆ g.support) :
f.degree ≤ g.degree
source
theorem Polynomial.degree_le_degree {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.coeff p.natDegree ≠ 0) :
p.degree ≤ q.degree
source
theorem Polynomial.natDegree_le_iff_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} :
p.natDegree ≤ n ↔ p.degree ≤ ↑n
source
theorem Polynomial.natDegree_lt_iff_degree_lt {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) :
p.natDegree < n ↔ p.degree < ↑n
source
theorem Polynomial.natDegree_le_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} :
p.degree ≤ ↑n → p.natDegree ≤ n

Alias of the reverse direction of `Polynomial.natDegree_le_iff_degree_le`.

source
theorem Polynomial.degree_le_of_natDegree_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} :
p.natDegree ≤ n → p.degree ≤ ↑n

Alias of the forward direction of `Polynomial.natDegree_le_iff_degree_le`.

source
theorem Polynomial.natDegree_le_natDegree {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {q : Polynomial S} (hpq : p.degree ≤ q.degree) :
p.natDegree ≤ q.natDegree
source
@[simp]
theorem Polynomial.degree_C {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) :
(C a).degree = 0
source
theorem Polynomial.degree_C_le {R : Type u} {a : R} [Semiring R] :
(C a).degree ≤ 0
source
theorem Polynomial.degree_C_lt {R : Type u} {a : R} [Semiring R] :
(C a).degree < 1
source
theorem Polynomial.degree_one_le {R : Type u} [Semiring R] :
degree 1 ≤ 0
source
@[simp]
theorem Polynomial.natDegree_C {R : Type u} [Semiring R] (a : R) :
(C a).natDegree = 0
source
@[simp]
theorem Polynomial.natDegree_one {R : Type u} [Semiring R] :
natDegree 1 = 0
source
@[simp]
theorem Polynomial.natDegree_natCast {R : Type u} [Semiring R] (n : ℕ) :
(↑n).natDegree = 0
source
@[simp]
theorem Polynomial.natDegree_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n).natDegree = 0
source
theorem Polynomial.degree_natCast_le {R : Type u} [Semiring R] (n : ℕ) :
(↑n).degree ≤ 0
source
@[simp]
theorem Polynomial.degree_monomial {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) :
((monomial n) a).degree = ↑n
source
@[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
source
theorem Polynomial.degree_C_mul_X {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) :
(C a * X).degree = 1
source
theorem Polynomial.degree_monomial_le {R : Type u} [Semiring R] (n : ℕ) (a : R) :
((monomial n) a).degree ≤ ↑n
source
theorem Polynomial.degree_C_mul_X_pow_le {R : Type u} [Semiring R] (n : ℕ) (a : R) :
(C a * X ^ n).degree ≤ ↑n
source
theorem Polynomial.degree_C_mul_X_le {R : Type u} [Semiring R] (a : R) :
(C a * X).degree ≤ 1
source
@[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
source
@[simp]
theorem Polynomial.natDegree_C_mul_X {R : Type u} [Semiring R] (a : R) (ha : a ≠ 0) :
(C a * X).natDegree = 1
source
@[simp]
theorem Polynomial.natDegree_monomial {R : Type u} [Semiring R] [DecidableEq R] (i : ℕ) (r : R) :
((monomial i) r).natDegree = if r = 0 then 0 else i
source
theorem Polynomial.natDegree_monomial_le {R : Type u} [Semiring R] (a : R) {m : ℕ} :
((monomial m) a).natDegree ≤ m
source
theorem Polynomial.natDegree_monomial_eq {R : Type u} [Semiring R] (i : ℕ) {r : R} (r0 : r ≠ 0) :
((monomial i) r).natDegree = i
source
theorem Polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hn : p.degree = ↑n) :
p.coeff n ≠ 0
source
theorem Polynomial.degree_X_pow_le {R : Type u} [Semiring R] (n : ℕ) :
(X ^ n).degree ≤ ↑n
source
theorem Polynomial.degree_X_le {R : Type u} [Semiring R] :
X.degree ≤ 1
source
theorem Polynomial.natDegree_X_le {R : Type u} [Semiring R] :
X.natDegree ≤ 1
source
theorem Polynomial.withBotSucc_degree_eq_natDegree_add_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p ≠ 0) :
p.degree.succ = p.natDegree + 1
source
@[simp]
theorem Polynomial.degree_one {R : Type u} [Semiring R] [Nontrivial R] :
degree 1 = 0
source
@[simp]
theorem Polynomial.degree_X {R : Type u} [Semiring R] [Nontrivial R] :
X.degree = 1
source
@[simp]
theorem Polynomial.natDegree_X {R : Type u} [Semiring R] [Nontrivial R] :
X.natDegree = 1
source
@[simp]
theorem Polynomial.degree_neg {R : Type u} [Ring R] (p : Polynomial R) :
(-p).degree = p.degree
source
theorem Polynomial.degree_neg_le_of_le {R : Type u} [Ring R] {a : WithBot ℕ} {p : Polynomial R} (hp : p.degree ≤ a) :
(-p).degree ≤ a
source
@[simp]
theorem Polynomial.natDegree_neg {R : Type u} [Ring R] (p : Polynomial R) :
(-p).natDegree = p.natDegree
source
theorem Polynomial.natDegree_neg_le_of_le {R : Type u} {m : ℕ} [Ring R] {p : Polynomial R} (hp : p.natDegree ≤ m) :
(-p).natDegree ≤ m
source
@[simp]
theorem Polynomial.natDegree_intCast {R : Type u} [Ring R] (n : ℤ) :
(↑n).natDegree = 0
source
theorem Polynomial.degree_intCast_le {R : Type u} [Ring R] (n : ℤ) :
(↑n).degree ≤ 0
source
@[simp]
theorem Polynomial.leadingCoeff_neg {R : Type u} [Ring R] (p : Polynomial R) :
(-p).leadingCoeff = -p.leadingCoeff
source
def Polynomial.nextCoeff {R : Type u} [Semiring R] (p : Polynomial R) :
R

The second-highest coefficient, or 0 for constants

Equations

- p.nextCoeff = if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)

Instances For

source
theorem Polynomial.nextCoeff_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0
source
theorem Polynomial.nextCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0
source
@[simp]
theorem Polynomial.nextCoeff_C_eq_zero {R : Type u} [Semiring R] (c : R) :
(C c).nextCoeff = 0
source
theorem Polynomial.nextCoeff_of_natDegree_pos {R : Type u} [Semiring R] {p : Polynomial R} (hp : 0 < p.natDegree) :
p.nextCoeff = p.coeff (p.natDegree - 1)
source
theorem Polynomial.degree_add_le {R : Type u} [Semiring R] (p q : Polynomial R) :
(p + q).degree ≤ max p.degree q.degree
source
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
source
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) :
(p + q).degree ≤ max a b
source
theorem Polynomial.natDegree_add_le {R : Type u} [Semiring R] (p q : Polynomial R) :
(p + q).natDegree ≤ max p.natDegree q.natDegree
source
theorem Polynomial.natDegree_add_le_of_degree_le {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) :
(p + q).natDegree ≤ n
source
theorem Polynomial.natDegree_add_le_of_le {R : Type u} {n m : ℕ} [Semiring R] {p q : Polynomial R} (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ n) :
(p + q).natDegree ≤ max m n
source
@[simp]
theorem Polynomial.leadingCoeff_zero {R : Type u} [Semiring R] :
leadingCoeff 0 = 0
source
@[simp]
theorem Polynomial.leadingCoeff_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.leadingCoeff = 0 ↔ p = 0
source
theorem Polynomial.leadingCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.leadingCoeff ≠ 0 ↔ p ≠ 0
source
theorem Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot {R : Type u} [Semiring R] {p : Polynomial R} :
p.leadingCoeff = 0 ↔ p.degree = ⊥
source
theorem Polynomial.natDegree_C_mul_X_pow_le {R : Type u} [Semiring R] (a : R) (n : ℕ) :
(C a * X ^ n).natDegree ≤ n
source
theorem Polynomial.degree_erase_le {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
(erase n p).degree ≤ p.degree
source
theorem Polynomial.degree_erase_lt {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) :
(erase p.natDegree p).degree < p.degree
source
theorem Polynomial.degree_update_le {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) :
(p.update n a).degree ≤ max p.degree ↑n
source
theorem Polynomial.degree_sum_le {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) :
(∑ i ∈ s, f i).degree ≤ s.sup fun (b : ι) => (f b).degree
source
theorem Polynomial.degree_mul_le {R : Type u} [Semiring R] (p q : Polynomial R) :
(p * q).degree ≤ p.degree + q.degree
source
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) :
(p * q).degree ≤ a + b
source
theorem Polynomial.degree_pow_le {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
(p ^ n).degree ≤ n • p.degree
source
theorem Polynomial.degree_pow_le_of_le {R : Type u} [Semiring R] {p : Polynomial R} {a : WithBot ℕ} (b : ℕ) (hp : p.degree ≤ a) :
(p ^ b).degree ≤ ↑b * a
source
@[simp]
theorem Polynomial.leadingCoeff_monomial {R : Type u} [Semiring R] (a : R) (n : ℕ) :
((monomial n) a).leadingCoeff = a
source
theorem Polynomial.leadingCoeff_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ℕ) :
(C a * X ^ n).leadingCoeff = a
source
theorem Polynomial.leadingCoeff_C_mul_X {R : Type u} [Semiring R] (a : R) :
(C a * X).leadingCoeff = a
source
@[simp]
theorem Polynomial.leadingCoeff_C {R : Type u} [Semiring R] (a : R) :
(C a).leadingCoeff = a
source
theorem Polynomial.leadingCoeff_X_pow {R : Type u} [Semiring R] (n : ℕ) :
(X ^ n).leadingCoeff = 1
source
theorem Polynomial.leadingCoeff_X {R : Type u} [Semiring R] :
X.leadingCoeff = 1
source
@[simp]
theorem Polynomial.monic_X_pow {R : Type u} [Semiring R] (n : ℕ) :
(X ^ n).Monic
source
@[simp]
theorem Polynomial.monic_X {R : Type u} [Semiring R] :
X.Monic
source
theorem Polynomial.leadingCoeff_one {R : Type u} [Semiring R] :
leadingCoeff 1 = 1
source
@[simp]
theorem Polynomial.monic_one {R : Type u} [Semiring R] :
Monic 1
source
theorem Polynomial.Monic.ne_zero {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p.Monic) :
p ≠ 0
source
theorem Polynomial.Monic.ne_zero_of_ne {R : Type u} [Semiring R] (h : 0 ≠ 1) {p : Polynomial R} (hp : p.Monic) :
p ≠ 0
source
theorem Polynomial.Monic.ne_zero_of_C {R : Type u} [Semiring R] [Nontrivial R] {c : R} (hc : (C c).Monic) :
c ≠ 0
source
theorem Polynomial.Monic.ne_zero_of_polynomial_ne {R : Type u} [Semiring R] {p q r : Polynomial R} (hp : p.Monic) (hne : q ≠ r) :
p ≠ 0
source
theorem Polynomial.natDegree_mul_le {R : Type u} [Semiring R] {p q : Polynomial R} :
(p * q).natDegree ≤ p.natDegree + q.natDegree
source
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) :
(p * q).natDegree ≤ m + n
source
theorem Polynomial.natDegree_pow_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} :
(p ^ n).natDegree ≤ n * p.natDegree
source
theorem Polynomial.natDegree_pow_le_of_le {R : Type u} {m : ℕ} [Semiring R] {p : Polynomial R} (n : ℕ) (hp : p.natDegree ≤ m) :
(p ^ n).natDegree ≤ n * m
source
theorem Polynomial.natDegree_eq_zero_iff_degree_le_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.natDegree = 0 ↔ p.degree ≤ 0
source
theorem Polynomial.degree_zero_le {R : Type u} [Semiring R] :
degree 0 ≤ 0
source
theorem Polynomial.degree_le_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : WithBot ℕ) :
f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
source
theorem Polynomial.degree_lt_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : ℕ) :
f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0
source
theorem Polynomial.natDegree_pos_iff_degree_pos {R : Type u} [Semiring R] {p : Polynomial R} :
0 < p.natDegree ↔ 0 < p.degree
source
@[simp]
theorem Polynomial.degree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) :
(X ^ n).degree = ↑n
source
@[simp]
theorem Polynomial.natDegree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) :
(X ^ n).natDegree = n
source
theorem Polynomial.degree_sub_le {R : Type u} [Ring R] (p q : Polynomial R) :
(p - q).degree ≤ max p.degree q.degree
source
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) :
(p - q).degree ≤ max a b
source
theorem Polynomial.natDegree_sub_le {R : Type u} [Ring R] (p q : Polynomial R) :
(p - q).natDegree ≤ max p.natDegree q.natDegree
source
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) :
(p - q).natDegree ≤ max m n
source
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) :
(p - q).degree < p.degree
source
theorem Polynomial.degree_X_sub_C_le {R : Type u} [Ring R] (r : R) :
(X - C r).degree ≤ 1
source
theorem Polynomial.natDegree_X_sub_C_le {R : Type u} [Ring R] (r : R) :
(X - C r).natDegree ≤ 1