# mathlibdocumentation

data.polynomial.degree.basic

# Theory of univariate polynomials

The definitions include degree, monic, leading_coeff

Results include

• degree_mul : The degree of the product is the sum of degrees
• leading_coeff_add_of_degree_eq and leading_coeff_add_of_degree_lt : The leading_coefficient of a sum is determined by the leading coefficients and degrees
def polynomial.degree {R : Type u} [semiring R] :

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
theorem polynomial.degree_lt_wf {R : Type u} [semiring R] :
well_founded (λ (p q : , p.degree < q.degree)

@[instance]
def polynomial.has_well_founded {R : Type u} [semiring R] :

Equations
def polynomial.nat_degree {R : Type u} [semiring R] :

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

Equations
def polynomial.leading_coeff {R : Type u} [semiring R] :
→ R

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

Equations
def polynomial.monic {R : Type u} [semiring R] :
→ Prop

a polynomial is monic if its leading coefficient is 1

Equations
theorem polynomial.monic_of_subsingleton {R : Type u} [semiring R] [subsingleton R] (p : polynomial R) :

theorem polynomial.monic.def {R : Type u} [semiring R] {p : polynomial R} :

@[instance]
def polynomial.monic.decidable {R : Type u} [semiring R] {p : polynomial R} [decidable_eq R] :

Equations
@[simp]
theorem polynomial.monic.leading_coeff {R : Type u} [semiring R] {p : polynomial R} :
p.monic

@[simp]
theorem polynomial.degree_zero {R : Type u} [semiring R] :

@[simp]
theorem polynomial.nat_degree_zero {R : Type u} [semiring R] :

theorem polynomial.degree_eq_bot {R : Type u} [semiring R] {p : polynomial R} :
p.degree = p = 0

theorem polynomial.degree_eq_nat_degree {R : Type u} [semiring R] {p : polynomial R} :
p 0p.degree = (p.nat_degree)

theorem polynomial.degree_eq_iff_nat_degree_eq {R : Type u} [semiring R] {p : polynomial R} {n : } :
p 0(p.degree = n p.nat_degree = n)

theorem polynomial.degree_eq_iff_nat_degree_eq_of_pos {R : Type u} [semiring R] {p : polynomial R} {n : } :
0 < n(p.degree = n p.nat_degree = n)

theorem polynomial.nat_degree_eq_of_degree_eq_some {R : Type u} [semiring R] {p : polynomial R} {n : } :
p.degree = np.nat_degree = n

@[simp]
theorem polynomial.degree_le_nat_degree {R : Type u} [semiring R] {p : polynomial R} :

theorem polynomial.nat_degree_eq_of_degree_eq {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] {q : polynomial S} :
p.degree = q.degree

theorem polynomial.le_degree_of_ne_zero {R : Type u} {n : } [semiring R] {p : polynomial R} :
p.coeff n 0n p.degree

theorem polynomial.le_nat_degree_of_ne_zero {R : Type u} {n : } [semiring R] {p : polynomial R} :
p.coeff n 0n p.nat_degree

theorem polynomial.degree_le_degree {R : Type u} [semiring R] {p q : polynomial R} :

theorem polynomial.degree_ne_of_nat_degree_ne {R : Type u} [semiring R] {p : polynomial R} {n : } :

theorem polynomial.nat_degree_le_of_degree_le {R : Type u} [semiring R] {p : polynomial R} {n : } :

theorem polynomial.nat_degree_le_nat_degree {R : Type u} [semiring R] {p q : polynomial R} :
p.degree q.degree

@[simp]
theorem polynomial.degree_C {R : Type u} {a : R} [semiring R] :
a 0.degree = 0

theorem polynomial.degree_C_le {R : Type u} {a : R} [semiring R] :

theorem polynomial.degree_one_le {R : Type u} [semiring R] :

@[simp]
theorem polynomial.nat_degree_C {R : Type u} [semiring R] (a : R) :
= 0

@[simp]
theorem polynomial.nat_degree_one {R : Type u} [semiring R] :

@[simp]
theorem polynomial.nat_degree_nat_cast {R : Type u} [semiring R] (n : ) :

@[simp]
theorem polynomial.degree_monomial {R : Type u} {a : R} [semiring R] (n : ) :
a 0((polynomial.C a) * .degree = n

theorem polynomial.degree_monomial_le {R : Type u} [semiring R] (n : ) (a : R) :

@[simp]
theorem polynomial.nat_degree_C_mul_X_pow {R : Type u} [semiring R] (n : ) (a : R) :
a 0((polynomial.C a) * .nat_degree = n

@[simp]
theorem polynomial.nat_degree_monomial {R : Type u} [semiring R] (i : ) (r : R) :
r 0 = i

theorem polynomial.coeff_eq_zero_of_degree_lt {R : Type u} {n : } [semiring R] {p : polynomial R} :
p.degree < np.coeff n = 0

theorem polynomial.coeff_eq_zero_of_nat_degree_lt {R : Type u} [semiring R] {p : polynomial R} {n : } :
p.nat_degree < np.coeff n = 0

@[simp]
theorem polynomial.coeff_nat_degree_succ_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p.coeff (p.nat_degree + 1) = 0

theorem polynomial.ite_le_nat_degree_coeff {R : Type u} [semiring R] (p : polynomial R) (n : ) (I : decidable (n < 1 + p.nat_degree)) :
ite (n < 1 + p.nat_degree) (p.coeff n) 0 = p.coeff n

theorem polynomial.as_sum_range {R : Type u} [semiring R] (p : polynomial R) :
p = ∑ (i : ) in finset.range (p.nat_degree + 1), (polynomial.C (p.coeff i)) *

theorem polynomial.as_sum_support {R : Type u} [semiring R] (p : polynomial R) :
p = ∑ (i : ) in p.support, (polynomial.C (p.coeff i)) *

theorem polynomial.sum_over_range' {R : Type u} {S : Type v} [semiring R] (p : polynomial R) {f : R → S} (h : ∀ (n : ), f n 0 = 0) (n : ) :
p.nat_degree < n f = ∑ (a : ) in , f a (p.coeff a)

We can reexpress a sum over p.support as a sum over range n, for any n satisfying p.nat_degree < n.

theorem polynomial.sum_over_range {R : Type u} {S : Type v} [semiring R] (p : polynomial R) {f : R → S} :
(∀ (n : ), f n 0 = 0) f = ∑ (a : ) in finset.range (p.nat_degree + 1), f a (p.coeff a)

We can reexpress a sum over p.support as a sum over range (p.nat_degree + 1).

theorem polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : } [semiring R] {p : polynomial R} :
p.degree = np.coeff n 0

theorem polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [semiring R] {p : polynomial R} :
p.degree = 1p =

theorem polynomial.degree_C_mul_X_pow_le {R : Type u} [semiring R] (r : R) (n : ) :

theorem polynomial.degree_X_pow_le {R : Type u} [semiring R] (n : ) :

theorem polynomial.degree_X_le {R : Type u} [semiring R] :

theorem polynomial.nat_degree_X_le {R : Type u} [semiring R] :

theorem polynomial.mem_support_C_mul_X_pow {R : Type u} [semiring R] {n a : } {c : R} :
a ((polynomial.C c) * .supporta = n

theorem polynomial.support_C_mul_X_pow {R : Type u} [semiring R] (c : R) (n : ) :

theorem polynomial.card_support_C_mul_X_pow_le_one {R : Type u} [semiring R] {c : R} {n : } :

theorem polynomial.le_nat_degree_of_mem_supp {R : Type u} [semiring R] {p : polynomial R} (a : ) :

theorem polynomial.le_degree_of_mem_supp {R : Type u} [semiring R] {p : polynomial R} (a : ) :
a p.supporta p.degree

theorem polynomial.nonempty_support_iff {R : Type u} [semiring R] {p : polynomial R} :

theorem polynomial.support_C_mul_X_pow_nonzero {R : Type u} [semiring R] {c : R} {n : } :
c 0((polynomial.C c) * .support = {n}

@[simp]
theorem polynomial.degree_one {R : Type u} [semiring R] [nontrivial R] :
1.degree = 0

@[simp]
theorem polynomial.degree_X {R : Type u} [semiring R] [nontrivial R] :

@[simp]
theorem polynomial.nat_degree_X {R : Type u} [semiring R] [nontrivial R] :

theorem polynomial.coeff_mul_X_sub_C {R : Type u} [ring R] {p : polynomial R} {r : R} {a : } :
(p * .coeff (a + 1) = p.coeff a - (p.coeff (a + 1)) * r

@[simp]
theorem polynomial.C_eq_int_cast {R : Type u} [ring R] (n : ) :

@[simp]
theorem polynomial.degree_neg {R : Type u} [ring R] (p : polynomial R) :

@[simp]
theorem polynomial.nat_degree_neg {R : Type u} [ring R] (p : polynomial R) :

@[simp]
theorem polynomial.nat_degree_int_cast {R : Type u} [ring R] (n : ) :

def polynomial.next_coeff {R : Type u} [semiring R] :
→ R

The second-highest coefficient, or 0 for constants

Equations
@[simp]
theorem polynomial.next_coeff_C_eq_zero {R : Type u} [semiring R] (c : R) :
= 0

theorem polynomial.ne_zero_of_degree_gt {R : Type u} [semiring R] {p : polynomial R} {n : with_bot } :
n < p.degreep 0

theorem polynomial.eq_C_of_degree_le_zero {R : Type u} [semiring R] {p : polynomial R} :
p.degree 0p = polynomial.C (p.coeff 0)

theorem polynomial.eq_C_of_degree_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p.degree = 0p = polynomial.C (p.coeff 0)

theorem polynomial.degree_le_zero_iff {R : Type u} [semiring R] {p : polynomial R} :

theorem polynomial.degree_add_le {R : Type u} [semiring R] (p q : polynomial R) :
(p + q).degree q.degree

@[simp]
theorem polynomial.leading_coeff_zero {R : Type u} [semiring R] :

@[simp]
theorem polynomial.leading_coeff_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p = 0

theorem polynomial.nat_degree_mem_support_of_nonzero {R : Type u} [semiring R] {p : polynomial R} :
p 0

theorem polynomial.nat_degree_eq_support_max' {R : Type u} [semiring R] {p : polynomial R} (h : p 0) :

theorem polynomial.nat_degree_C_mul_X_pow_le {R : Type u} [semiring R] (a : R) (n : ) :

theorem polynomial.nat_degree_C_mul_X_pow_of_nonzero {R : Type u} [semiring R] {a : R} (n : ) :
a 0((polynomial.C a) * .nat_degree = n

theorem polynomial.degree_add_eq_of_degree_lt {R : Type u} [semiring R] {p q : polynomial R} :
p.degree < q.degree(p + q).degree = q.degree

theorem polynomial.degree_add_C {R : Type u} {a : R} [semiring R] {p : polynomial R} :
0 < p.degree(p + .degree = p.degree

theorem polynomial.degree_erase_le {R : Type u} [semiring R] (p : polynomial R) (n : ) :

theorem polynomial.degree_erase_lt {R : Type u} [semiring R] {p : polynomial R} :
p 0

theorem polynomial.degree_sum_le {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι → ) :
(∑ (i : ι) in s, f i).degree s.sup (λ (b : ι), (f b).degree)

theorem polynomial.degree_mul_le {R : Type u} [semiring R] (p q : polynomial R) :

theorem polynomial.degree_pow_le {R : Type u} [semiring R] (p : polynomial R) (n : ) :

@[simp]
theorem polynomial.leading_coeff_monomial {R : Type u} [semiring R] (a : R) (n : ) :

@[simp]
theorem polynomial.leading_coeff_monomial' {R : Type u} [semiring R] (a : R) (n : ) :

@[simp]
theorem polynomial.leading_coeff_C {R : Type u} [semiring R] (a : R) :

@[simp]
theorem polynomial.leading_coeff_X {R : Type u} [semiring R] :

@[simp]
theorem polynomial.monic_X {R : Type u} [semiring R] :

@[simp]
theorem polynomial.leading_coeff_one {R : Type u} [semiring R] :

@[simp]
theorem polynomial.monic_one {R : Type u} [semiring R] :

theorem polynomial.monic.ne_zero_of_zero_ne_one {R : Type u} [semiring R] (h : 0 1) {p : polynomial R} :
p.monicp 0

theorem polynomial.monic.ne_zero {R : Type u_1} [semiring R] [nontrivial R] {p : polynomial R} :
p.monicp 0

theorem polynomial.leading_coeff_add_of_degree_eq {R : Type u} [semiring R] {p q : polynomial R} :
p.degree = q.degree 0(p + q).leading_coeff =

@[simp]
theorem polynomial.coeff_mul_degree_add_degree {R : Type u} [semiring R] (p q : polynomial R) :

theorem polynomial.degree_mul' {R : Type u} [semiring R] {p q : polynomial R} :
0(p * q).degree = p.degree + q.degree

theorem polynomial.nat_degree_mul' {R : Type u} [semiring R] {p q : polynomial R} :
0(p * q).nat_degree =

theorem polynomial.leading_coeff_mul' {R : Type u} [semiring R] {p q : polynomial R} :

theorem polynomial.leading_coeff_pow' {R : Type u} {n : } [semiring R] {p : polynomial R} :

theorem polynomial.degree_pow' {R : Type u} [semiring R] {p : polynomial R} {n : } :
0(p ^ n).degree = n •ℕ p.degree

theorem polynomial.nat_degree_pow' {R : Type u} [semiring R] {p : polynomial R} {n : } :
0(p ^ n).nat_degree = n * p.nat_degree

@[simp]
theorem polynomial.leading_coeff_X_pow {R : Type u} [semiring R] (n : ) :
= 1

theorem polynomial.nat_degree_mul_le {R : Type u} [semiring R] {p q : polynomial R} :

theorem polynomial.subsingleton_of_monic_zero {R : Type u} [semiring R] :
0.monic((∀ (p q : , p = q) ∀ (a b : R), a = b)

theorem polynomial.zero_le_degree_iff {R : Type u} [semiring R] {p : polynomial R} :
0 p.degree p 0

theorem polynomial.degree_nonneg_iff_ne_zero {R : Type u} [semiring R] {p : polynomial R} :
0 p.degree p 0

theorem polynomial.degree_le_iff_coeff_zero {R : Type u} [semiring R] (f : polynomial R) (n : with_bot ) :
f.degree n ∀ (m : ), n < mf.coeff m = 0

theorem polynomial.degree_lt_degree_mul_X {R : Type u} [semiring R] {p : polynomial R} :
p 0p.degree < .degree

@[simp]
theorem polynomial.degree_X_pow {R : Type u} [semiring R] [nontrivial R] (n : ) :

theorem polynomial.not_is_unit_X {R : Type u} [semiring R] [nontrivial R] :

theorem polynomial.degree_sub_le {R : Type u} [ring R] (p q : polynomial R) :
(p - q).degree q.degree

theorem polynomial.degree_sub_lt {R : Type u} [ring R] {p q : polynomial R} :
p.degree = q.degreep 0(p - q).degree < p.degree

theorem polynomial.nat_degree_X_sub_C_le {R : Type u} [ring R] {r : R} :

@[simp]
theorem polynomial.degree_X_sub_C {R : Type u} [nontrivial R] [ring R] (a : R) :

@[simp]
theorem polynomial.nat_degree_X_sub_C {R : Type u} [nontrivial R] [ring R] (x : R) :

@[simp]
theorem polynomial.next_coeff_X_sub_C {R : Type u} [nontrivial R] [ring R] (c : R) :

theorem polynomial.degree_X_pow_sub_C {R : Type u} [nontrivial R] [ring R] {n : } (hn : 0 < n) (a : R) :

theorem polynomial.X_pow_sub_C_ne_zero {R : Type u} [nontrivial R] [ring R] {n : } (hn : 0 < n) (a : R) :
0

theorem polynomial.X_sub_C_ne_zero {R : Type u} [nontrivial R] [ring R] (r : R) :

theorem polynomial.nat_degree_X_pow_sub_C {R : Type u} [nontrivial R] [ring R] {n : } (hn : 0 < n) {r : R} :

@[simp]
theorem polynomial.degree_mul {R : Type u} {p q : polynomial R} :
(p * q).degree = p.degree + q.degree

@[simp]
theorem polynomial.degree_pow {R : Type u} (p : polynomial R) (n : ) :
(p ^ n).degree = n •ℕ p.degree

@[simp]
theorem polynomial.leading_coeff_mul {R : Type u} (p q : polynomial R) :

@[simp]
polynomial.leading_coeff bundled as a monoid_hom when R is an integral_domain, and thus leading_coeff is multiplicative