Lemmas for calculating the degree of univariate polynomials

Main results

• degree_mul : The degree of the product is the sum of degrees
• leadingCoeff_add_of_degree_eq and leadingCoeff_add_of_degree_lt : The leading coefficient of a sum is determined by the leading coefficients and degrees

theorem Polynomial.supDegree_eq_degree {R : Type u} [Semiring R] (p : Polynomial R) : AddMonoidAlgebra.supDegree WithBot.some p.toFinsupp = p.degree

theorem Polynomial.degree_lt_wf {R : Type u} [Semiring R] : WellFounded fun (p q : Polynomial R) => p.degree < q.degree

@[implicit_reducible]

instance Polynomial.instWellFoundedRelation {R : Type u} [Semiring R] : WellFoundedRelation (Polynomial R)

theorem Polynomial.monic_of_subsingleton {R : Type u} [Semiring R] [Subsingleton R] (p : Polynomial R) : p.Monic

theorem Polynomial.degree_of_subsingleton {R : Type u} [Semiring R] {p : Polynomial R} [Subsingleton R] : p.degree = ⊥

theorem Polynomial.natDegree_of_subsingleton {R : Type u} [Semiring R] {p : Polynomial R} [Subsingleton R] : p.natDegree = 0

theorem Polynomial.le_natDegree_of_ne_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) : n ≤ p.natDegree

theorem Polynomial.degree_eq_of_le_of_coeff_ne_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.degree ≤ ↑n) (p1 : p.coeff n ≠ 0) : p.degree = ↑n

theorem Polynomial.natDegree_eq_of_le_of_coeff_ne_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) (p1 : p.coeff n ≠ 0) : p.natDegree = n

theorem Polynomial.natDegree_lt_natDegree {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} {q : Polynomial S} (hp : p ≠ 0) (hpq : p.degree < q.degree) : p.natDegree < q.natDegree

theorem Polynomial.natDegree_eq_natDegree {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} {q : Polynomial S} (hpq : p.degree = q.degree) : p.natDegree = q.natDegree

theorem Polynomial.coeff_eq_zero_of_degree_lt {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.degree < ↑n) : p.coeff n = 0

theorem Polynomial.coeff_eq_zero_of_natDegree_lt {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.natDegree < n) : p.coeff n = 0

theorem Polynomial.ext_iff_natDegree_le {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) : p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i

theorem Polynomial.ext_iff_degree_le {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.degree ≤ ↑n) (hq : q.degree ≤ ↑n) : p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i

@[simp]

theorem Polynomial.coeff_natDegree_succ_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff (p.natDegree + 1) = 0

theorem Polynomial.ite_le_natDegree_coeff {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (I : Decidable (n < 1 + p.natDegree)) : (if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n

theorem Polynomial.coeff_mul_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} {r : R} {a : ℕ} : (p * (X - C r)).coeff (a + 1) = p.coeff a - p.coeff (a + 1) * r

theorem Polynomial.coeff_X_sub_C_mul {R : Type u} [Ring R] {p : Polynomial R} {r : R} {a : ℕ} : ((X - C r) * p).coeff (a + 1) = p.coeff a - r * p.coeff (a + 1)

theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : p.coeff q.natDegree = 0

theorem Polynomial.ne_zero_of_degree_gt {R : Type u} [Semiring R] {p : Polynomial R} {n : WithBot ℕ} (h : n < p.degree) : p ≠ 0

theorem Polynomial.ne_zero_of_degree_ge_degree {R : Type u} [Semiring R] {p q : Polynomial R} (hpq : p.degree ≤ q.degree) (hp : p ≠ 0) : q ≠ 0

theorem Polynomial.ne_zero_of_natDegree_gt {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : n < p.natDegree) : p ≠ 0

theorem Polynomial.degree_lt_degree {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.natDegree < q.natDegree) : p.degree < q.degree

theorem Polynomial.natDegree_lt_natDegree_iff {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p ≠ 0) : p.natDegree < q.natDegree ↔ p.degree < q.degree

theorem Polynomial.eq_C_of_degree_le_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree ≤ 0) : p = C (p.coeff 0)

theorem Polynomial.eq_C_of_degree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree = 0) : p = C (p.coeff 0)

theorem Polynomial.degree_le_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} : p.degree ≤ 0 ↔ p = C (p.coeff 0)

theorem Polynomial.degree_add_eq_left_of_degree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p + q).degree = p.degree

theorem Polynomial.degree_add_eq_right_of_degree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p + q).degree = q.degree

theorem Polynomial.natDegree_add_eq_left_of_degree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p + q).natDegree = p.natDegree

theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.natDegree < p.natDegree) : (p + q).natDegree = p.natDegree

theorem Polynomial.natDegree_add_eq_right_of_degree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p + q).natDegree = q.natDegree

theorem Polynomial.natDegree_add_eq_right_of_natDegree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.natDegree < q.natDegree) : (p + q).natDegree = q.natDegree

theorem Polynomial.degree_add_C {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : 0 < p.degree) : (p + C a).degree = p.degree

@[simp]

theorem Polynomial.natDegree_add_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} : (p + C a).natDegree = p.natDegree

@[simp]

theorem Polynomial.natDegree_C_add {R : Type u} [Semiring R] {p : Polynomial R} {a : R} : (C a + p).natDegree = p.natDegree

theorem Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff + q.leadingCoeff ≠ 0) : (p + q).degree = max p.degree q.degree

theorem Polynomial.natDegree_eq_of_natDegree_add_lt_left {R : Type u} [Semiring R] (p q : Polynomial R) (H : (p + q).natDegree < p.natDegree) : p.natDegree = q.natDegree

theorem Polynomial.natDegree_eq_of_natDegree_add_lt_right {R : Type u} [Semiring R] (p q : Polynomial R) (H : (p + q).natDegree < q.natDegree) : p.natDegree = q.natDegree

theorem Polynomial.natDegree_eq_of_natDegree_add_eq_zero {R : Type u} [Semiring R] (p q : Polynomial R) (H : (p + q).natDegree = 0) : p.natDegree = q.natDegree

theorem Polynomial.monic_of_natDegree_le_of_coeff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.natDegree ≤ n) (p1 : p.coeff n = 1) : p.Monic

theorem Polynomial.monic_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.degree ≤ ↑n) (p1 : p.coeff n = 1) : p.Monic

@[deprecated Polynomial.monic_of_degree_le (since := "2025-10-24")]

theorem Polynomial.monic_of_degree_le_of_coeff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.degree ≤ ↑n) (p1 : p.coeff n = 1) : p.Monic

Alias of Polynomial.monic_of_degree_le.

theorem Polynomial.leadingCoeff_add_of_degree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p + q).leadingCoeff = q.leadingCoeff

theorem Polynomial.leadingCoeff_add_of_degree_lt' {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p + q).leadingCoeff = p.leadingCoeff

theorem Polynomial.leadingCoeff_add_of_degree_eq {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree = q.degree) (hlc : p.leadingCoeff + q.leadingCoeff ≠ 0) : (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff

@[simp]

theorem Polynomial.coeff_mul_degree_add_degree {R : Type u} [Semiring R] (p q : Polynomial R) : (p * q).coeff (p.natDegree + q.natDegree) = p.leadingCoeff * q.leadingCoeff

theorem Polynomial.degree_mul' {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).degree = p.degree + q.degree

theorem Polynomial.Monic.degree_mul {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) : (p * q).degree = p.degree + q.degree

theorem Polynomial.natDegree_mul' {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree

theorem Polynomial.leadingCoeff_mul' {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

theorem Polynomial.Monic.leadingCoeff_C_mul {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (C r * p).leadingCoeff = r

theorem Polynomial.leadingCoeff_pow' {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n

theorem Polynomial.degree_pow' {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.leadingCoeff ^ n ≠ 0 → (p ^ n).degree = n • p.degree

theorem Polynomial.natDegree_pow' {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.leadingCoeff ^ n ≠ 0) : (p ^ n).natDegree = n * p.natDegree

theorem Polynomial.leadingCoeff_monic_mul {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) : (p * q).leadingCoeff = q.leadingCoeff

theorem Polynomial.leadingCoeff_mul_monic {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) : (p * q).leadingCoeff = p.leadingCoeff

theorem Polynomial.degree_C_mul_of_isUnit {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (C a * p).degree = p.degree

theorem Polynomial.degree_mul_C_of_isUnit {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (p * C a).degree = p.degree

theorem Polynomial.natDegree_C_mul_of_isUnit {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (C a * p).natDegree = p.natDegree

theorem Polynomial.natDegree_mul_C_of_isUnit {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (p * C a).natDegree = p.natDegree

theorem Polynomial.leadingCoeff_C_mul_of_isUnit {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (C a * p).leadingCoeff = a * p.leadingCoeff

theorem Polynomial.leadingCoeff_mul_C_of_isUnit {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (p * C a).leadingCoeff = p.leadingCoeff * a

@[simp]

theorem Polynomial.leadingCoeff_mul_X_pow {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : (p * X ^ n).leadingCoeff = p.leadingCoeff

@[simp]

theorem Polynomial.leadingCoeff_mul_X {R : Type u} [Semiring R] {p : Polynomial R} : (p * X).leadingCoeff = p.leadingCoeff

@[simp]

theorem Polynomial.coeff_pow_mul_natDegree {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n

theorem Polynomial.coeff_mul_add_eq_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

theorem Polynomial.degree_smul_le {R : Type u} [Semiring R] {S : Type u_2} [SMulZeroClass S R] (a : S) (p : Polynomial R) : (a • p).degree ≤ p.degree

theorem Polynomial.natDegree_smul_le {R : Type u} [Semiring R] {S : Type u_2} [SMulZeroClass S R] (a : S) (p : Polynomial R) : (a • p).natDegree ≤ p.natDegree

theorem Polynomial.degree_smul_of_isRightRegular_leadingCoeff {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (ha : a ≠ 0) (hp : IsRightRegular p.leadingCoeff) : (a • p).degree = p.degree

theorem Polynomial.degree_lt_degree_mul_X {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.degree < (p * X).degree

theorem Polynomial.eq_C_of_natDegree_le_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 0) : p = C (p.coeff 0)

theorem Polynomial.eq_C_of_natDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree = 0) : p = C (p.coeff 0)

theorem Polynomial.natDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.natDegree = 0 ↔ ∃ (x : R), C x = p

theorem Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p = C (p.coeff 0) ↔ p.natDegree = 0

theorem Polynomial.eq_one_of_monic_natDegree_zero {R : Type u} [Semiring R] {p : Polynomial R} (hf : p.Monic) (hfd : p.natDegree = 0) : p = 1

@[simp]

theorem Polynomial.Monic.natDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} (hf : p.Monic) : p.natDegree = 0 ↔ p = 1

theorem Polynomial.degree_sum_fin_lt {R : Type u} [Semiring R] {n : ℕ} (f : Fin n → R) : (∑ i : Fin n, C (f i) * X ^ ↑i).degree < ↑n

theorem Polynomial.degree_C_lt_degree_C_mul_X {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) : (C b).degree < (C a * X).degree

@[simp]

theorem Polynomial.natDegree_mul_X {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p ≠ 0) : (p * X).natDegree = p.natDegree + 1

@[simp]

theorem Polynomial.natDegree_X_mul {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p ≠ 0) : (X * p).natDegree = p.natDegree + 1

@[simp]

theorem Polynomial.natDegree_mul_X_pow {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) (hp : p ≠ 0) : (p * X ^ n).natDegree = p.natDegree + n

@[simp]

theorem Polynomial.natDegree_X_pow_mul {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) (hp : p ≠ 0) : (X ^ n * p).natDegree = p.natDegree + n

theorem Polynomial.natDegree_X_pow_le {R : Type u_1} [Semiring R] (n : ℕ) : (X ^ n).natDegree ≤ n

theorem Polynomial.not_isUnit_X {R : Type u} [Semiring R] [Nontrivial R] : ¬IsUnit X

@[simp]

theorem Polynomial.degree_mul_X {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} : (p * X).degree = p.degree + 1

@[simp]

theorem Polynomial.degree_mul_X_pow {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) : (p * X ^ n).degree = p.degree + ↑n

theorem Polynomial.degree_sub_C {R : Type u} {a : R} [Ring R] {p : Polynomial R} (hp : 0 < p.degree) : (p - C a).degree = p.degree

@[simp]

theorem Polynomial.natDegree_sub_C {R : Type u} [Ring R] {p : Polynomial R} {a : R} : (p - C a).natDegree = p.natDegree

theorem Polynomial.leadingCoeff_sub_of_degree_lt {R : Type u} [Ring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p - q).leadingCoeff = p.leadingCoeff

theorem Polynomial.leadingCoeff_sub_of_degree_lt' {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p - q).leadingCoeff = -q.leadingCoeff

theorem Polynomial.leadingCoeff_sub_of_degree_eq {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree = q.degree) (hlc : p.leadingCoeff ≠ q.leadingCoeff) : (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

theorem Polynomial.degree_sub_eq_left_of_degree_lt {R : Type u} [Ring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p - q).degree = p.degree

theorem Polynomial.degree_sub_eq_right_of_degree_lt {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p - q).degree = q.degree

theorem Polynomial.natDegree_sub_eq_left_of_natDegree_lt {R : Type u} [Ring R] {p q : Polynomial R} (h : q.natDegree < p.natDegree) : (p - q).natDegree = p.natDegree

theorem Polynomial.natDegree_sub_eq_right_of_natDegree_lt {R : Type u} [Ring R] {p q : Polynomial R} (h : p.natDegree < q.natDegree) : (p - q).natDegree = q.natDegree

@[simp]

theorem Polynomial.degree_X_add_C {R : Type u} [Nontrivial R] [Semiring R] (a : R) : (X + C a).degree = 1

theorem Polynomial.natDegree_X_add_C {R : Type u} [Nontrivial R] [Semiring R] (x : R) : (X + C x).natDegree = 1

@[simp]

theorem Polynomial.nextCoeff_X_add_C {S : Type v} [Semiring S] (c : S) : (X + C c).nextCoeff = c

theorem Polynomial.degree_X_pow_add_C {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} (hn : 0 < n) (a : R) : (X ^ n + C a).degree = ↑n

theorem Polynomial.X_pow_add_C_ne_zero {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} (hn : 0 < n) (a : R) : X ^ n + C a ≠ 0

theorem Polynomial.X_add_C_ne_zero {R : Type u} [Nontrivial R] [Semiring R] (r : R) : X + C r ≠ 0

theorem Polynomial.zero_notMem_multiset_map_X_add_C {R : Type u} [Nontrivial R] [Semiring R] {α : Type u_1} (m : Multiset α) (f : α → R) : 0 ∉ Multiset.map (fun (a : α) => X + C (f a)) m

theorem Polynomial.natDegree_X_pow_add_C {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} {r : R} : (X ^ n + C r).natDegree = n

theorem Polynomial.X_pow_add_C_ne_one {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} (hn : 0 < n) (a : R) : X ^ n + C a ≠ 1

theorem Polynomial.X_add_C_ne_one {R : Type u} [Nontrivial R] [Semiring R] (r : R) : X + C r ≠ 1

@[simp]

theorem Polynomial.leadingCoeff_X_pow_add_C {R : Type u} [Semiring R] {n : ℕ} (hn : 0 < n) {r : R} : (X ^ n + C r).leadingCoeff = 1

@[simp]

theorem Polynomial.leadingCoeff_X_add_C {S : Type v} [Semiring S] (r : S) : (X + C r).leadingCoeff = 1

@[simp]

theorem Polynomial.leadingCoeff_X_pow_add_one {R : Type u} [Semiring R] {n : ℕ} (hn : 0 < n) : (X ^ n + 1).leadingCoeff = 1

@[simp]

theorem Polynomial.leadingCoeff_pow_X_add_C {R : Type u} [Semiring R] (r : R) (i : ℕ) : ((X + C r) ^ i).leadingCoeff = 1

@[simp]

theorem Polynomial.degree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} : (p * q).degree = p.degree + q.degree

def Polynomial.degreeMonoidHom {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] : Polynomial R →* Multiplicative (WithBot ℕ)

degree as a monoid homomorphism between R[X] and Multiplicative (WithBot ℕ). This is useful to prove results about multiplication and degree.

@[simp]

theorem Polynomial.degree_pow {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (p : Polynomial R) (n : ℕ) : (p ^ n).degree = n • p.degree

@[simp]

theorem Polynomial.leadingCoeff_mul {R : Type u} [Semiring R] [NoZeroDivisors R] (p q : Polynomial R) : (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

def Polynomial.leadingCoeffHom {R : Type u} [Semiring R] [NoZeroDivisors R] : Polynomial R →* R

Polynomial.leadingCoeff bundled as a MonoidHom when R has NoZeroDivisors, and thus leadingCoeff is multiplicative

@[simp]

theorem Polynomial.leadingCoeffHom_apply {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) : leadingCoeffHom p = p.leadingCoeff

@[simp]

theorem Polynomial.leadingCoeff_pow {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ℕ) : (p ^ n).leadingCoeff = p.leadingCoeff ^ n

theorem Polynomial.leadingCoeff_dvd_leadingCoeff {R : Type u} [Semiring R] [NoZeroDivisors R] {a p : Polynomial R} (hap : a ∣ p) : a.leadingCoeff ∣ p.leadingCoeff

theorem Polynomial.degree_le_mul_left {R : Type u} [Semiring R] [NoZeroDivisors R] {q : Polynomial R} (p : Polynomial R) (hq : q ≠ 0) : p.degree ≤ (p * q).degree

theorem Polynomial.Monic.natDegree_pos {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : 0 < p.natDegree ↔ p ≠ 1

theorem Polynomial.Monic.degree_pos {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : 0 < p.degree ↔ p ≠ 1

@[simp]

theorem Polynomial.leadingCoeff_X_pow_sub_C {R : Type u} [Ring R] {n : ℕ} (hn : 0 < n) {r : R} : (X ^ n - C r).leadingCoeff = 1

@[simp]

theorem Polynomial.leadingCoeff_X_pow_sub_one {R : Type u} [Ring R] {n : ℕ} (hn : 0 < n) : (X ^ n - 1).leadingCoeff = 1

@[simp]

theorem Polynomial.degree_X_sub_C {R : Type u} [Ring R] [Nontrivial R] (a : R) : (X - C a).degree = 1

theorem Polynomial.natDegree_X_sub_C {R : Type u} [Ring R] [Nontrivial R] (x : R) : (X - C x).natDegree = 1

@[simp]

theorem Polynomial.nextCoeff_X_sub_C {S : Type v} [Ring S] (c : S) : (X - C c).nextCoeff = -c

theorem Polynomial.degree_X_pow_sub_C {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} (hn : 0 < n) (a : R) : (X ^ n - C a).degree = ↑n

theorem Polynomial.X_pow_sub_C_ne_zero {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} (hn : 0 < n) (a : R) : X ^ n - C a ≠ 0

theorem Polynomial.X_sub_C_ne_zero {R : Type u} [Ring R] [Nontrivial R] (r : R) : X - C r ≠ 0

theorem Polynomial.zero_notMem_multiset_map_X_sub_C {R : Type u} [Ring R] [Nontrivial R] {α : Type u_1} (m : Multiset α) (f : α → R) : 0 ∉ Multiset.map (fun (a : α) => X - C (f a)) m

theorem Polynomial.natDegree_X_pow_sub_C {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} {r : R} : (X ^ n - C r).natDegree = n

@[simp]

theorem Polynomial.leadingCoeff_X_sub_C {S : Type v} [Ring S] (r : S) : (X - C r).leadingCoeff = 1