# Theory of degrees of polynomials #

Some of the main results include

• natDegree_comp_le : The degree of the composition is at most the product of degrees
theorem Polynomial.natDegree_comp_le {R : Type u} [] {p : } {q : } :
(p.comp q).natDegree p.natDegree * q.natDegree
theorem Polynomial.natDegree_comp_eq_of_mul_ne_zero {R : Type u} [] {p : } {q : } (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree 0) :
(p.comp q).natDegree = p.natDegree * q.natDegree
theorem Polynomial.degree_pos_of_root {R : Type u} {a : R} [] {p : } (hp : p 0) (h : p.IsRoot a) :
0 < p.degree
theorem Polynomial.natDegree_le_iff_coeff_eq_zero {R : Type u} {n : } [] {p : } :
p.natDegree n ∀ (N : ), n < Np.coeff N = 0
theorem Polynomial.natDegree_add_le_iff_left {R : Type u} [] {n : } (p : ) (q : ) (qn : q.natDegree n) :
(p + q).natDegree n p.natDegree n
theorem Polynomial.natDegree_add_le_iff_right {R : Type u} [] {n : } (p : ) (q : ) (pn : p.natDegree n) :
(p + q).natDegree n q.natDegree n
theorem Polynomial.natDegree_C_mul_le {R : Type u} [] (a : R) (f : ) :
(Polynomial.C a * f).natDegree f.natDegree
theorem Polynomial.natDegree_mul_C_le {R : Type u} [] (f : ) (a : R) :
(f * Polynomial.C a).natDegree f.natDegree
theorem Polynomial.eq_natDegree_of_le_mem_support {R : Type u} {n : } [] {p : } (pn : p.natDegree n) (ns : n p.support) :
p.natDegree = n
theorem Polynomial.natDegree_C_mul_eq_of_mul_eq_one {R : Type u} {a : R} [] {p : } {ai : R} (au : ai * a = 1) :
(Polynomial.C a * p).natDegree = p.natDegree
theorem Polynomial.natDegree_mul_C_eq_of_mul_eq_one {R : Type u} {a : R} [] {p : } {ai : R} (au : a * ai = 1) :
(p * Polynomial.C a).natDegree = p.natDegree
theorem Polynomial.natDegree_mul_C_eq_of_mul_ne_zero {R : Type u} {a : R} [] {p : } (h : p.leadingCoeff * a 0) :
(p * Polynomial.C a).natDegree = p.natDegree

Although not explicitly stated, the assumptions of lemma nat_degree_mul_C_eq_of_mul_ne_zero force the polynomial p to be non-zero, via p.leading_coeff ≠ 0.

theorem Polynomial.natDegree_C_mul_eq_of_mul_ne_zero {R : Type u} {a : R} [] {p : } (h : a * p.leadingCoeff 0) :
(Polynomial.C a * p).natDegree = p.natDegree

Although not explicitly stated, the assumptions of lemma nat_degree_C_mul_eq_of_mul_ne_zero force the polynomial p to be non-zero, via p.leading_coeff ≠ 0.

theorem Polynomial.natDegree_add_coeff_mul {R : Type u} [] (f : ) (g : ) :
(f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
theorem Polynomial.natDegree_lt_coeff_mul {R : Type u} {m : } {n : } [] {p : } {q : } (h : p.natDegree + q.natDegree < m + n) :
(p * q).coeff (m + n) = 0
theorem Polynomial.coeff_mul_of_natDegree_le {R : Type u} {m : } {n : } [] {p : } {q : } (pm : p.natDegree m) (qn : q.natDegree n) :
(p * q).coeff (m + n) = p.coeff m * q.coeff n
theorem Polynomial.coeff_pow_of_natDegree_le {R : Type u} {m : } {n : } [] {p : } (pn : p.natDegree n) :
(p ^ m).coeff (m * n) = p.coeff n ^ m
theorem Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le {R : Type u} {m : } {n : } [] {p : } {o : } (pn : p.natDegree n) (mno : m * n o) :
(p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
theorem Polynomial.coeff_add_eq_left_of_lt {R : Type u} {n : } [] {p : } {q : } (qn : q.natDegree < n) :
(p + q).coeff n = p.coeff n
theorem Polynomial.coeff_add_eq_right_of_lt {R : Type u} {n : } [] {p : } {q : } (pn : p.natDegree < n) :
(p + q).coeff n = q.coeff n
theorem Polynomial.degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [] (f : S) (s : ) (h : {i : S | i s f i 0}.Pairwise (Ne on Polynomial.degree f)) :
(s.sum f).degree = s.sup fun (i : S) => (f i).degree
theorem Polynomial.natDegree_sum_eq_of_disjoint {R : Type u} {S : Type v} [] (f : S) (s : ) (h : {i : S | i s f i 0}.Pairwise (Ne on Polynomial.natDegree f)) :
(s.sum f).natDegree = s.sup fun (i : S) => (f i).natDegree
theorem Polynomial.natDegree_pos_of_eval₂_root {R : Type u} {S : Type v} [] [] {p : } (hp : p 0) (f : R →+* S) {z : S} (hz : = 0) (inj : ∀ (x : R), f x = 0x = 0) :
0 < p.natDegree
theorem Polynomial.degree_pos_of_eval₂_root {R : Type u} {S : Type v} [] [] {p : } (hp : p 0) (f : R →+* S) {z : S} (hz : = 0) (inj : ∀ (x : R), f x = 0x = 0) :
0 < p.degree
@[simp]
theorem Polynomial.coe_lt_degree {R : Type u} [] {p : } {n : } :
n < p.degree n < p.natDegree
@[simp]
theorem Polynomial.degree_map_eq_iff {R : Type u} {S : Type v} [] [] {f : R →+* S} {p : } :
(Polynomial.map f p).degree = p.degree f p.leadingCoeff 0 p = 0
@[simp]
theorem Polynomial.natDegree_map_eq_iff {R : Type u} {S : Type v} [] [] {f : R →+* S} {p : } :
(Polynomial.map f p).natDegree = p.natDegree f p.leadingCoeff 0 p.natDegree = 0
theorem Polynomial.natDegree_pos_of_nextCoeff_ne_zero {R : Type u} [] {p : } (h : p.nextCoeff 0) :
0 < p.natDegree
theorem Polynomial.natDegree_sub {R : Type u} [Ring R] {p : } {q : } :
(p - q).natDegree = (q - p).natDegree
theorem Polynomial.natDegree_sub_le_iff_left {R : Type u} {n : } [Ring R] {p : } {q : } (qn : q.natDegree n) :
(p - q).natDegree n p.natDegree n
theorem Polynomial.natDegree_sub_le_iff_right {R : Type u} {n : } [Ring R] {p : } {q : } (pn : p.natDegree n) :
(p - q).natDegree n q.natDegree n
theorem Polynomial.coeff_sub_eq_left_of_lt {R : Type u} {n : } [Ring R] {p : } {q : } (dg : q.natDegree < n) :
(p - q).coeff n = p.coeff n
theorem Polynomial.coeff_sub_eq_neg_right_of_lt {R : Type u} {n : } [Ring R] {p : } {q : } (df : p.natDegree < n) :
(p - q).coeff n = -q.coeff n
@[simp]
theorem Polynomial.nextCoeff_C_mul_X_add_C {R : Type u} [] {a : R} (ha : a 0) (c : R) :
(Polynomial.C a * Polynomial.X + Polynomial.C c).nextCoeff = c
theorem Polynomial.natDegree_eq_one {R : Type u} [] {p : } :
p.natDegree = 1 ∃ (a : R), a 0 ∃ (b : R), Polynomial.C a * Polynomial.X + Polynomial.C b = p
theorem Polynomial.degree_mul_C {R : Type u} [] {p : } {a : R} [] (a0 : a 0) :
(p * Polynomial.C a).degree = p.degree
theorem Polynomial.degree_C_mul {R : Type u} [] {p : } {a : R} [] (a0 : a 0) :
(Polynomial.C a * p).degree = p.degree
theorem Polynomial.natDegree_mul_C {R : Type u} [] {p : } {a : R} [] (a0 : a 0) :
(p * Polynomial.C a).natDegree = p.natDegree
theorem Polynomial.natDegree_C_mul {R : Type u} [] {p : } {a : R} [] (a0 : a 0) :
(Polynomial.C a * p).natDegree = p.natDegree
theorem Polynomial.natDegree_comp {R : Type u} [] {p : } {q : } [] :
(p.comp q).natDegree = p.natDegree * q.natDegree
@[simp]
theorem Polynomial.natDegree_iterate_comp {R : Type u} [] {p : } {q : } [] (k : ) :
(p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
theorem Polynomial.leadingCoeff_comp {R : Type u} [] {p : } {q : } [] (hq : q.natDegree 0) :

Useful lemmas for the "monicization" of a nonzero polynomial p.

@[simp]
theorem Polynomial.irreducible_mul_leadingCoeff_inv {K : Type u_1} [] {p : } :
@[simp]
theorem Polynomial.dvd_mul_leadingCoeff_inv {K : Type u_1} [] {p : } {q : } (hp0 : p 0) :
q p * Polynomial.C p.leadingCoeff⁻¹ q p
theorem Polynomial.monic_mul_leadingCoeff_inv {K : Type u_1} [] {p : } (h : p 0) :
@[simp]
theorem Polynomial.degree_leadingCoeff_inv {K : Type u_1} [] {p : } (hp0 : p 0) :