# 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 : } :
theorem Polynomial.degree_pos_of_root {R : Type u} {a : R} [] {p : } (hp : p 0) (h : ) :
theorem Polynomial.natDegree_le_iff_coeff_eq_zero {R : Type u} {n : } [] {p : } :
∀ (N : ), n < N = 0
theorem Polynomial.natDegree_add_le_iff_left {R : Type u} [] {n : } (p : ) (q : ) (qn : ) :
theorem Polynomial.natDegree_add_le_iff_right {R : Type u} [] {n : } (p : ) (q : ) (pn : ) :
theorem Polynomial.natDegree_C_mul_le {R : Type u} [] (a : R) (f : ) :
Polynomial.natDegree (Polynomial.C a * f)
theorem Polynomial.natDegree_mul_C_le {R : Type u} [] (f : ) (a : R) :
Polynomial.natDegree (f * Polynomial.C a)
theorem Polynomial.eq_natDegree_of_le_mem_support {R : Type u} {n : } [] {p : } (pn : ) (ns : ) :
theorem Polynomial.natDegree_C_mul_eq_of_mul_eq_one {R : Type u} {a : R} [] {p : } {ai : R} (au : ai * a = 1) :
Polynomial.natDegree (Polynomial.C a * p) =
theorem Polynomial.natDegree_mul_C_eq_of_mul_eq_one {R : Type u} {a : R} [] {p : } {ai : R} (au : a * ai = 1) :
Polynomial.natDegree (p * Polynomial.C a) =
theorem Polynomial.natDegree_mul_C_eq_of_mul_ne_zero {R : Type u} {a : R} [] {p : } (h : ) :
Polynomial.natDegree (p * Polynomial.C a) =

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 : ) :
Polynomial.natDegree (Polynomial.C a * p) =

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 : ) :
theorem Polynomial.natDegree_lt_coeff_mul {R : Type u} {m : } {n : } [] {p : } {q : } (h : ) :
Polynomial.coeff (p * q) (m + n) = 0
theorem Polynomial.coeff_mul_of_natDegree_le {R : Type u} {m : } {n : } [] {p : } {q : } (pm : ) (qn : ) :
Polynomial.coeff (p * q) (m + n) =
theorem Polynomial.coeff_pow_of_natDegree_le {R : Type u} {m : } {n : } [] {p : } (pn : ) :
Polynomial.coeff (p ^ m) (m * n) = ^ m
theorem Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le {R : Type u} {m : } {n : } [] {p : } {o : } (pn : ) (mno : m * n o) :
Polynomial.coeff (p ^ m) o = if o = m * n then ^ m else 0
theorem Polynomial.coeff_add_eq_left_of_lt {R : Type u} {n : } [] {p : } {q : } (qn : ) :
theorem Polynomial.coeff_add_eq_right_of_lt {R : Type u} {n : } [] {p : } {q : } (pn : ) :
theorem Polynomial.degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [] (f : S) (s : ) (h : Set.Pairwise {i : S | i s f i 0} (Ne on Polynomial.degree f)) :
= Finset.sup s fun (i : S) => Polynomial.degree (f i)
theorem Polynomial.natDegree_sum_eq_of_disjoint {R : Type u} {S : Type v} [] (f : S) (s : ) (h : Set.Pairwise {i : S | i s f i 0} (Ne on Polynomial.natDegree f)) :
= Finset.sup s fun (i : S) => Polynomial.natDegree (f i)
theorem Polynomial.natDegree_bit0 {R : Type u} [] (a : ) :
theorem Polynomial.natDegree_bit1 {R : Type u} [] (a : ) :
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) :
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) :
@[simp]
theorem Polynomial.coe_lt_degree {R : Type u} [] {p : } {n : } :
@[simp]
theorem Polynomial.degree_map_eq_iff {R : Type u} {S : Type v} [] [] {f : R →+* S} {p : } :
0 p = 0
@[simp]
theorem Polynomial.natDegree_map_eq_iff {R : Type u} {S : Type v} [] [] {f : R →+* S} {p : } :
0
theorem Polynomial.natDegree_sub {R : Type u} [Ring R] {p : } {q : } :
theorem Polynomial.natDegree_sub_le_iff_left {R : Type u} {n : } [Ring R] {p : } {q : } (qn : ) :
theorem Polynomial.natDegree_sub_le_iff_right {R : Type u} {n : } [Ring R] {p : } {q : } (pn : ) :
theorem Polynomial.coeff_sub_eq_left_of_lt {R : Type u} {n : } [Ring R] {p : } {q : } (dg : ) :
theorem Polynomial.coeff_sub_eq_neg_right_of_lt {R : Type u} {n : } [Ring R] {p : } {q : } (df : ) :
theorem Polynomial.degree_mul_C {R : Type u} [] [] {p : } {a : R} (a0 : a 0) :
Polynomial.degree (p * Polynomial.C a) =
theorem Polynomial.degree_C_mul {R : Type u} [] [] {p : } {a : R} (a0 : a 0) :
Polynomial.degree (Polynomial.C a * p) =
theorem Polynomial.natDegree_mul_C {R : Type u} [] [] {p : } {a : R} (a0 : a 0) :
Polynomial.natDegree (p * Polynomial.C a) =
theorem Polynomial.natDegree_C_mul {R : Type u} [] [] {p : } {a : R} (a0 : a 0) :
Polynomial.natDegree (Polynomial.C a * p) =
@[simp]
theorem Polynomial.nextCoeff_C_mul_X_add_C {R : Type u} [] {a : R} (ha : a 0) (c : R) :
Polynomial.nextCoeff (Polynomial.C a * Polynomial.X + Polynomial.C c) = c
theorem Polynomial.natDegree_eq_one {R : Type u} [] {p : } :
∃ (a : R), a 0 ∃ (b : R), Polynomial.C a * Polynomial.X + Polynomial.C b = p
theorem Polynomial.natDegree_comp {R : Type u} [] [] {p : } {q : } :
@[simp]
theorem Polynomial.natDegree_iterate_comp {R : Type u} [] [] {p : } {q : } (k : ) :
theorem Polynomial.leadingCoeff_comp {R : Type u} [] [] {p : } {q : } (hq : ) :

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

@[simp]
theorem Polynomial.irreducible_mul_leadingCoeff_inv {K : Type u_1} [] {p : } :
Irreducible (p * Polynomial.C )
@[simp]
theorem Polynomial.dvd_mul_leadingCoeff_inv {K : Type u_1} [] {p : } {q : } (hp0 : p 0) :
q p * Polynomial.C q p
theorem Polynomial.monic_mul_leadingCoeff_inv {K : Type u_1} [] {p : } (h : p 0) :
Polynomial.Monic (p * Polynomial.C )
@[simp]
theorem Polynomial.degree_leadingCoeff_inv {K : Type u_1} [] {p : } (hp0 : p 0) :
Polynomial.degree (Polynomial.C ) = 0
theorem Polynomial.degree_mul_leadingCoeff_inv {K : Type u_1} [] (p : ) {q : } (h : q 0) :
Polynomial.degree (p * Polynomial.C ) =
theorem Polynomial.natDegree_mul_leadingCoeff_inv {K : Type u_1} [] (p : ) {q : } (h : q 0) :
Polynomial.natDegree (p * Polynomial.C ) =
theorem Polynomial.degree_mul_leadingCoeff_self_inv {K : Type u_1} [] (p : ) :
Polynomial.degree (p * Polynomial.C ) =
theorem Polynomial.natDegree_mul_leadingCoeff_self_inv {K : Type u_1} [] (p : ) :
Polynomial.natDegree (p * Polynomial.C ) =
@[simp]