# 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

source
theorem Polynomial.natDegree_comp_le {R : Type u} [Semiring R] {p q : Polynomial R} :
(p.comp q).natDegree ≤ p.natDegree * q.natDegree
source
theorem Polynomial.natDegree_comp_eq_of_mul_ne_zero {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) :
(p.comp q).natDegree = p.natDegree * q.natDegree
source
theorem Polynomial.degree_pos_of_root {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (h : p.IsRoot a) :
0 < p.degree
source
theorem Polynomial.natDegree_le_iff_coeff_eq_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} :
p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
source
theorem Polynomial.natDegree_add_le_iff_left {R : Type u} [Semiring R] {n : ℕ} (p q : Polynomial R) (qn : q.natDegree ≤ n) :
(p + q).natDegree ≤ n ↔ p.natDegree ≤ n
source
theorem Polynomial.natDegree_add_le_iff_right {R : Type u} [Semiring R] {n : ℕ} (p q : Polynomial R) (pn : p.natDegree ≤ n) :
(p + q).natDegree ≤ n ↔ q.natDegree ≤ n
source
theorem Polynomial.natDegree_C_mul_le {R : Type u} [Semiring R] (a : R) (f : Polynomial R) :
(C a * f).natDegree ≤ f.natDegree
source
theorem Polynomial.natDegree_mul_C_le {R : Type u} [Semiring R] (f : Polynomial R) (a : R) :
(f * C a).natDegree ≤ f.natDegree
source
theorem Polynomial.eq_natDegree_of_le_mem_support {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) (ns : n ∈ p.support) :
p.natDegree = n
source
theorem Polynomial.natDegree_C_mul_eq_of_mul_eq_one {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {ai : R} (au : ai * a = 1) :
(C a * p).natDegree = p.natDegree
source
theorem Polynomial.natDegree_mul_C_eq_of_mul_eq_one {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {ai : R} (au : a * ai = 1) :
(p * C a).natDegree = p.natDegree
source
theorem Polynomial.natDegree_mul_C_eq_of_mul_ne_zero {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : p.leadingCoeff * a ≠ 0) :
(p * C a).natDegree = p.natDegree

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

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

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

source
theorem Polynomial.degree_C_mul_of_mul_ne_zero {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : a * p.leadingCoeff ≠ 0) :
(C a * p).degree = p.degree
source
theorem Polynomial.natDegree_add_coeff_mul {R : Type u} [Semiring R] (f g : Polynomial R) :
(f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
source
theorem Polynomial.natDegree_lt_coeff_mul {R : Type u} {m n : ℕ} [Semiring R] {p q : Polynomial R} (h : p.natDegree + q.natDegree < m + n) :
(p * q).coeff (m + n) = 0
source
@[deprecated Polynomial.coeff_mul_add_eq_of_natDegree_le (since := "2025-08-14")]
theorem Polynomial.coeff_mul_of_natDegree_le {R : Type u} [Semiring R] {df dg : ℕ} {f g : Polynomial R} (hdf : f.natDegree ≤ df) (hdg : g.natDegree ≤ dg) :
(f * g).coeff (df + dg) = f.coeff df * g.coeff dg

Alias of `Polynomial.coeff_mul_add_eq_of_natDegree_le`.

source
theorem Polynomial.coeff_pow_of_natDegree_le {R : Type u} {m n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) :
(p ^ m).coeff (m * n) = p.coeff n ^ m
source
theorem Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le {R : Type u} {m n : ℕ} [Semiring R] {p : Polynomial R} {o : ℕ} (pn : p.natDegree ≤ n) (mno : m * n ≤ o) :
(p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
source
theorem Polynomial.coeff_add_eq_left_of_lt {R : Type u} {n : ℕ} [Semiring R] {p q : Polynomial R} (qn : q.natDegree < n) :
(p + q).coeff n = p.coeff n
source
theorem Polynomial.coeff_add_eq_right_of_lt {R : Type u} {n : ℕ} [Semiring R] {p q : Polynomial R} (pn : p.natDegree < n) :
(p + q).coeff n = q.coeff n
source
theorem Polynomial.degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i : S | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (degree ∘ f))) :
(s.sum f).degree = s.sup fun (i : S) => (f i).degree
source
theorem Polynomial.natDegree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i : S | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (natDegree ∘ f))) :
(s.sum f).natDegree = s.sup fun (i : S) => (f i).natDegree
source
theorem Polynomial.natDegree_pos_of_eval₂_root {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) :
0 < p.natDegree
source
theorem Polynomial.degree_pos_of_eval₂_root {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) :
0 < p.degree
source
@[simp]
theorem Polynomial.coe_lt_degree {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} :
↑n < p.degree ↔ n < p.natDegree
source
@[simp]
theorem Polynomial.degree_map_eq_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
(map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
source
@[simp]
theorem Polynomial.natDegree_map_eq_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
(map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
source
theorem Polynomial.degree_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) :
(map f p).degree = p.degree
source
theorem Polynomial.natDegree_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) :
(map f p).natDegree = p.natDegree
source
theorem Polynomial.leadingCoeff_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) :
(map f p).leadingCoeff = f p.leadingCoeff
source
theorem Polynomial.nextCoeff_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) :
(map f p).nextCoeff = f p.nextCoeff
source
theorem Polynomial.degree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) :
(map f p).degree = p.degree
source
theorem Polynomial.natDegree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) :
(map f p).natDegree = p.natDegree
source
theorem Polynomial.leadingCoeff_map_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) :
(map f p).leadingCoeff = f p.leadingCoeff
source
theorem Polynomial.nextCoeff_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) :
(map f p).nextCoeff = f p.nextCoeff
source
theorem Polynomial.natDegree_pos_of_nextCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.nextCoeff ≠ 0) :
0 < p.natDegree
source
theorem Polynomial.natDegree_sub {R : Type u} [Ring R] {p q : Polynomial R} :
(p - q).natDegree = (q - p).natDegree
source
theorem Polynomial.natDegree_sub_le_iff_left {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (qn : q.natDegree ≤ n) :
(p - q).natDegree ≤ n ↔ p.natDegree ≤ n
source
theorem Polynomial.natDegree_sub_le_iff_right {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (pn : p.natDegree ≤ n) :
(p - q).natDegree ≤ n ↔ q.natDegree ≤ n
source
theorem Polynomial.coeff_sub_eq_left_of_lt {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (dg : q.natDegree < n) :
(p - q).coeff n = p.coeff n
source
theorem Polynomial.coeff_sub_eq_neg_right_of_lt {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (df : p.natDegree < n) :
(p - q).coeff n = -q.coeff n
source
@[simp]
theorem Polynomial.nextCoeff_C_mul_X_add_C {R : Type u} [Semiring R] {a : R} (ha : a ≠ 0) (c : R) :
(C a * X + C c).nextCoeff = c
source
theorem Polynomial.natDegree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} :
p.natDegree = 1 ↔ ∃ (a : R), a ≠ 0 ∧ ∃ (b : R), C a * X + C b = p
source
theorem Polynomial.subsingleton_isRoot_of_natDegree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} [IsLeftCancelMulZero R] (h : p.natDegree = 1) :
{x : R | p.IsRoot x}.Subsingleton
source
theorem Polynomial.degree_mul_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) :
(p * C a).degree = p.degree
source
theorem Polynomial.degree_C_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) :
(C a * p).degree = p.degree
source
theorem Polynomial.natDegree_mul_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) :
(p * C a).natDegree = p.natDegree
source
theorem Polynomial.natDegree_C_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) :
(C a * p).natDegree = p.natDegree
source
theorem Polynomial.natDegree_comp {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] :
(p.comp q).natDegree = p.natDegree * q.natDegree
source
@[simp]
theorem Polynomial.natDegree_iterate_comp {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (k : ℕ) :
(p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
source
theorem Polynomial.leadingCoeff_comp {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (hq : q.natDegree ≠ 0) :
(p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
source
@[simp]
theorem Polynomial.nextCoeff_C_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] :
(C a * p).nextCoeff = a * p.nextCoeff
source
@[simp]
theorem Polynomial.nextCoeff_mul_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] :
(p * C a).nextCoeff = p.nextCoeff * a
source
@[simp]
theorem Polynomial.comp_neg_X_leadingCoeff_eq {R : Type u} [Ring R] (p : Polynomial R) :
(p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff
source
theorem Polynomial.comp_eq_zero_iff {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} :
p.comp q = 0 ↔ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

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

source
@[simp]
theorem Polynomial.irreducible_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} :
Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p
source
theorem Polynomial.dvd_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p q : Polynomial K} (hp0 : p ≠ 0) :
q ∣ p * C p.leadingCoeff⁻¹ ↔ q ∣ p
source
theorem Polynomial.monic_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} (h : p ≠ 0) :
(p * C p.leadingCoeff⁻¹).Monic
source
theorem Polynomial.degree_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} (hp0 : p ≠ 0) :
(C p.leadingCoeff⁻¹).degree = 0
source
theorem Polynomial.degree_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q ≠ 0) :
(p * C q.leadingCoeff⁻¹).degree = p.degree
source
theorem Polynomial.natDegree_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q ≠ 0) :
(p * C q.leadingCoeff⁻¹).natDegree = p.natDegree
source
theorem Polynomial.degree_mul_leadingCoeff_self_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) :
(p * C p.leadingCoeff⁻¹).degree = p.degree
source
theorem Polynomial.natDegree_mul_leadingCoeff_self_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) :
(p * C p.leadingCoeff⁻¹).natDegree = p.natDegree
source
@[simp]
theorem Polynomial.degree_add_degree_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) :
p.degree + (C p.leadingCoeff⁻¹).degree = p.degree