Theory of univariate polynomials

The definitions include degree, Monic, leadingCoeff

Results include

• 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

def Polynomial.degree {R : Type u} [Semiring R] (p : Polynomial R) : WithBot ℕ

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

• p.degree = p.support.max

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

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

Equations

• Polynomial.instWellFoundedRelation = { rel := fun (p q : Polynomial R) => p.degree < q.degree, wf := ⋯ }

def Polynomial.natDegree {R : Type u} [Semiring R] (p : Polynomial R) : ℕ

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

Equations

• p.natDegree = WithBot.unbot' 0 p.degree

def Polynomial.leadingCoeff {R : Type u} [Semiring R] (p : Polynomial R) : R

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

Equations

• p.leadingCoeff = p.coeff p.natDegree

def Polynomial.Monic {R : Type u} [Semiring R] (p : Polynomial R) : Prop

a polynomial is Monic if its leading coefficient is 1

Equations

• p.Monic = (p.leadingCoeff = 1)

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

theorem Polynomial.Monic.def {R : Type u} [Semiring R] {p : Polynomial R} : p.Monic ↔ p.leadingCoeff = 1

instance Polynomial.Monic.decidable {R : Type u} [Semiring R] {p : Polynomial R} [DecidableEq R] : Decidable p.Monic

Equations

• Polynomial.Monic.decidable = id inferInstance

@[simp]

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

theorem Polynomial.Monic.coeff_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p.coeff p.natDegree = 1

@[simp]

theorem Polynomial.degree_zero {R : Type u} [Semiring R] : Polynomial.degree 0 = ⊥

@[simp]

theorem Polynomial.natDegree_zero {R : Type u} [Semiring R] : Polynomial.natDegree 0 = 0

@[simp]

theorem Polynomial.coeff_natDegree {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff p.natDegree = p.leadingCoeff

@[simp]

theorem Polynomial.degree_eq_bot {R : Type u} [Semiring R] {p : Polynomial R} : p.degree = ⊥ ↔ p = 0

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.degree_eq_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.degree = ↑p.natDegree

theorem Polynomial.supDegree_eq_natDegree {R : Type u} [Semiring R] (p : Polynomial R) : AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

theorem Polynomial.degree_eq_iff_natDegree_eq {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hp : p ≠ 0) : p.degree = ↑n ↔ p.natDegree = n

theorem Polynomial.degree_eq_iff_natDegree_eq_of_pos {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : 0 < n) : p.degree = ↑n ↔ p.natDegree = n

theorem Polynomial.natDegree_eq_of_degree_eq_some {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.degree = ↑n) : p.natDegree = n

theorem Polynomial.degree_ne_of_natDegree_ne {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.natDegree ≠ n → p.degree ≠ ↑n

@[simp]

theorem Polynomial.degree_le_natDegree {R : Type u} [Semiring R] {p : Polynomial R} : p.degree ≤ ↑p.natDegree

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

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

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.le_natDegree_of_mem_supp {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → a ≤ 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.degree_mono {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : Polynomial R} {g : Polynomial S} (h : f.support ⊆ g.support) : f.degree ≤ g.degree

theorem Polynomial.supp_subset_range {R : Type u} {m : ℕ} [Semiring R] {p : Polynomial R} (h : p.natDegree < m) : p.support ⊆ Finset.range m

theorem Polynomial.supp_subset_range_natDegree_succ {R : Type u} [Semiring R] {p : Polynomial R} : p.support ⊆ Finset.range (p.natDegree + 1)

theorem Polynomial.degree_le_degree {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (h : q.coeff p.natDegree ≠ 0) : p.degree ≤ q.degree

theorem Polynomial.natDegree_le_iff_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.natDegree ≤ n ↔ p.degree ≤ ↑n

theorem Polynomial.natDegree_lt_iff_degree_lt {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.natDegree < n ↔ p.degree < ↑n

theorem Polynomial.natDegree_le_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.degree ≤ ↑n → p.natDegree ≤ n

Alias of the reverse direction of Polynomial.natDegree_le_iff_degree_le.

theorem Polynomial.degree_le_of_natDegree_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.natDegree ≤ n → p.degree ≤ ↑n

Alias of the forward direction of Polynomial.natDegree_le_iff_degree_le.

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

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

@[simp]

theorem Polynomial.degree_C {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a).degree = 0

theorem Polynomial.degree_C_le {R : Type u} {a : R} [Semiring R] : (Polynomial.C a).degree ≤ 0

theorem Polynomial.degree_C_lt {R : Type u} {a : R} [Semiring R] : (Polynomial.C a).degree < 1

theorem Polynomial.degree_one_le {R : Type u} [Semiring R] : Polynomial.degree 1 ≤ 0

@[simp]

theorem Polynomial.natDegree_C {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).natDegree = 0

@[simp]

theorem Polynomial.natDegree_one {R : Type u} [Semiring R] : Polynomial.natDegree 1 = 0

@[simp]

theorem Polynomial.natDegree_natCast {R : Type u} [Semiring R] (n : ℕ) : (↑n).natDegree = 0

theorem Polynomial.degree_natCast_le {R : Type u} [Semiring R] (n : ℕ) : (↑n).degree ≤ 0

@[simp]

theorem Polynomial.degree_monomial {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) : ((Polynomial.monomial n) a).degree = ↑n

@[simp]

theorem Polynomial.degree_C_mul_X_pow {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ n).degree = ↑n

theorem Polynomial.degree_C_mul_X {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X).degree = 1

theorem Polynomial.degree_monomial_le {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).degree ≤ ↑n

theorem Polynomial.degree_C_mul_X_pow_le {R : Type u} [Semiring R] (n : ℕ) (a : R) : (Polynomial.C a * Polynomial.X ^ n).degree ≤ ↑n

theorem Polynomial.degree_C_mul_X_le {R : Type u} [Semiring R] (a : R) : (Polynomial.C a * Polynomial.X).degree ≤ 1

@[simp]

theorem Polynomial.natDegree_C_mul_X_pow {R : Type u} [Semiring R] (n : ℕ) (a : R) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ n).natDegree = n

@[simp]

theorem Polynomial.natDegree_C_mul_X {R : Type u} [Semiring R] (a : R) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X).natDegree = 1

@[simp]

theorem Polynomial.natDegree_monomial {R : Type u} [Semiring R] [DecidableEq R] (i : ℕ) (r : R) : ((Polynomial.monomial i) r).natDegree = if r = 0 then 0 else i

theorem Polynomial.natDegree_monomial_le {R : Type u} [Semiring R] (a : R) {m : ℕ} : ((Polynomial.monomial m) a).natDegree ≤ m

theorem Polynomial.natDegree_monomial_eq {R : Type u} [Semiring R] (i : ℕ) {r : R} (r0 : r ≠ 0) : ((Polynomial.monomial i) r).natDegree = i

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 : Polynomial R} {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 : Polynomial R} {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.as_sum_support {R : Type u} [Semiring R] (p : Polynomial R) : p = p.support.sum fun (i : ℕ) => (Polynomial.monomial i) (p.coeff i)

theorem Polynomial.as_sum_support_C_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) : p = p.support.sum fun (i : ℕ) => Polynomial.C (p.coeff i) * Polynomial.X ^ i

theorem Polynomial.sum_over_range' {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) (n : ℕ) (w : p.natDegree < n) : p.sum f = (Finset.range n).sum fun (a : ℕ) => f a (p.coeff a)

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

theorem Polynomial.sum_over_range {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) : p.sum f = (Finset.range (p.natDegree + 1)).sum fun (a : ℕ) => f a (p.coeff a)

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

theorem Polynomial.sum_fin {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) {n : ℕ} {p : Polynomial R} (hn : p.degree < ↑n) : (Finset.univ.sum fun (i : Fin n) => f (↑i) (p.coeff ↑i)) = p.sum f

theorem Polynomial.as_sum_range' {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (w : p.natDegree < n) : p = (Finset.range n).sum fun (i : ℕ) => (Polynomial.monomial i) (p.coeff i)

theorem Polynomial.as_sum_range {R : Type u} [Semiring R] (p : Polynomial R) : p = (Finset.range (p.natDegree + 1)).sum fun (i : ℕ) => (Polynomial.monomial i) (p.coeff i)

theorem Polynomial.as_sum_range_C_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) : p = (Finset.range (p.natDegree + 1)).sum fun (i : ℕ) => Polynomial.C (p.coeff i) * Polynomial.X ^ i

theorem Polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hn : p.degree = ↑n) : p.coeff n ≠ 0

theorem Polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree ≤ 1) : p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)

theorem Polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree = 1) : p = Polynomial.C p.leadingCoeff * Polynomial.X + Polynomial.C (p.coeff 0)

theorem Polynomial.eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 1) : p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)

theorem Polynomial.Monic.eq_X_add_C {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 1) : p = Polynomial.X + Polynomial.C (p.coeff 0)

theorem Polynomial.exists_eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 1) : ∃ (a : R) (b : R), p = Polynomial.C a * Polynomial.X + Polynomial.C b

theorem Polynomial.degree_X_pow_le {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).degree ≤ ↑n

theorem Polynomial.degree_X_le {R : Type u} [Semiring R] : Polynomial.X.degree ≤ 1

theorem Polynomial.natDegree_X_le {R : Type u} [Semiring R] : Polynomial.X.natDegree ≤ 1

theorem Polynomial.mem_support_C_mul_X_pow {R : Type u} [Semiring R] {n : ℕ} {a : ℕ} {c : R} (h : a ∈ (Polynomial.C c * Polynomial.X ^ n).support) : a = n

theorem Polynomial.card_support_C_mul_X_pow_le_one {R : Type u} [Semiring R] {c : R} {n : ℕ} : (Polynomial.C c * Polynomial.X ^ n).support.card ≤ 1

theorem Polynomial.card_supp_le_succ_natDegree {R : Type u} [Semiring R] (p : Polynomial R) : p.support.card ≤ p.natDegree + 1

theorem Polynomial.le_degree_of_mem_supp {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → ↑a ≤ p.degree

theorem Polynomial.nonempty_support_iff {R : Type u} [Semiring R] {p : Polynomial R} : p.support.Nonempty ↔ p ≠ 0

@[simp]

theorem Polynomial.degree_one {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.degree 1 = 0

@[simp]

theorem Polynomial.degree_X {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.degree = 1

@[simp]

theorem Polynomial.natDegree_X {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.natDegree = 1

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

@[simp]

theorem Polynomial.degree_neg {R : Type u} [Ring R] (p : Polynomial R) : (-p).degree = p.degree

theorem Polynomial.degree_neg_le_of_le {R : Type u} [Ring R] {a : WithBot ℕ} {p : Polynomial R} (hp : p.degree ≤ a) : (-p).degree ≤ a

@[simp]

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

theorem Polynomial.natDegree_neg_le_of_le {R : Type u} {m : ℕ} [Ring R] {p : Polynomial R} (hp : p.natDegree ≤ m) : (-p).natDegree ≤ m

@[simp]

theorem Polynomial.natDegree_intCast {R : Type u} [Ring R] (n : ℤ) : (↑n).natDegree = 0

theorem Polynomial.degree_intCast_le {R : Type u} [Ring R] (n : ℤ) : (↑n).degree ≤ 0

@[simp]

theorem Polynomial.leadingCoeff_neg {R : Type u} [Ring R] (p : Polynomial R) : (-p).leadingCoeff = -p.leadingCoeff

def Polynomial.nextCoeff {R : Type u} [Semiring R] (p : Polynomial R) : R

The second-highest coefficient, or 0 for constants

Equations

• p.nextCoeff = if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)

theorem Polynomial.nextCoeff_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0

theorem Polynomial.nextCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0

@[simp]

theorem Polynomial.nextCoeff_C_eq_zero {R : Type u} [Semiring R] (c : R) : (Polynomial.C c).nextCoeff = 0

theorem Polynomial.nextCoeff_of_natDegree_pos {R : Type u} [Semiring R] {p : Polynomial R} (hp : 0 < p.natDegree) : p.nextCoeff = p.coeff (p.natDegree - 1)

theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (h : p.natDegree < q.natDegree) : p.degree < q.degree

theorem Polynomial.natDegree_lt_natDegree_iff {R : Type u} [Semiring R] {p : Polynomial R} {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 = Polynomial.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 = Polynomial.C (p.coeff 0)

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

theorem Polynomial.degree_add_le {R : Type u} [Semiring R] (p : Polynomial R) (q : Polynomial R) : (p + q).degree ≤ max p.degree q.degree

theorem Polynomial.degree_add_le_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {n : ℕ} (hp : p.degree ≤ ↑n) (hq : q.degree ≤ ↑n) : (p + q).degree ≤ ↑n

theorem Polynomial.degree_add_le_of_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {a : WithBot ℕ} {b : WithBot ℕ} (hp : p.degree ≤ a) (hq : q.degree ≤ b) : (p + q).degree ≤ max a b

theorem Polynomial.natDegree_add_le {R : Type u} [Semiring R] (p : Polynomial R) (q : Polynomial R) : (p + q).natDegree ≤ max p.natDegree q.natDegree

theorem Polynomial.natDegree_add_le_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) : (p + q).natDegree ≤ n

theorem Polynomial.natDegree_add_le_of_le {R : Type u} {n : ℕ} {m : ℕ} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ n) : (p + q).natDegree ≤ max m n

@[simp]

theorem Polynomial.leadingCoeff_zero {R : Type u} [Semiring R] : Polynomial.leadingCoeff 0 = 0

@[simp]

theorem Polynomial.leadingCoeff_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.leadingCoeff = 0 ↔ p = 0

theorem Polynomial.leadingCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.leadingCoeff ≠ 0 ↔ p ≠ 0

theorem Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot {R : Type u} [Semiring R] {p : Polynomial R} : p.leadingCoeff = 0 ↔ p.degree = ⊥

theorem Polynomial.natDegree_le_pred {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hf : p.natDegree ≤ n) (hn : p.coeff n = 0) : p.natDegree ≤ n - 1

theorem Polynomial.natDegree_mem_support_of_nonzero {R : Type u} [Semiring R] {p : Polynomial R} (H : p ≠ 0) : p.natDegree ∈ p.support

theorem Polynomial.natDegree_eq_support_max' {R : Type u} [Semiring R] {p : Polynomial R} (h : p ≠ 0) : p.natDegree = p.support.max' ⋯

theorem Polynomial.natDegree_C_mul_X_pow_le {R : Type u} [Semiring R] (a : R) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).natDegree ≤ n

theorem Polynomial.degree_add_eq_left_of_degree_lt {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (h : p.degree < q.degree) : (p + q).degree = q.degree

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

theorem Polynomial.natDegree_add_eq_right_of_natDegree_lt {R : Type u} [Semiring R] {p : Polynomial R} {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 + Polynomial.C a).degree = p.degree

@[simp]

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

@[simp]

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

theorem Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R) (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 : Polynomial R) (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 : Polynomial R) (q : Polynomial R) (H : (p + q).natDegree = 0) : p.natDegree = q.natDegree

theorem Polynomial.degree_erase_le {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.erase n p).degree ≤ p.degree

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

theorem Polynomial.degree_update_le {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (p.update n a).degree ≤ max p.degree ↑n

theorem Polynomial.degree_sum_le {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) : (s.sum fun (i : ι) => f i).degree ≤ s.sup fun (b : ι) => (f b).degree

theorem Polynomial.degree_mul_le {R : Type u} [Semiring R] (p : Polynomial R) (q : Polynomial R) : (p * q).degree ≤ p.degree + q.degree

theorem Polynomial.degree_mul_le_of_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {a : WithBot ℕ} {b : WithBot ℕ} (hp : p.degree ≤ a) (hq : q.degree ≤ b) : (p * q).degree ≤ a + b

theorem Polynomial.degree_pow_le {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (p ^ n).degree ≤ n • p.degree

theorem Polynomial.degree_pow_le_of_le {R : Type u} [Semiring R] {p : Polynomial R} {a : WithBot ℕ} (b : ℕ) (hp : p.degree ≤ a) : (p ^ b).degree ≤ ↑b * a

@[simp]

theorem Polynomial.leadingCoeff_monomial {R : Type u} [Semiring R] (a : R) (n : ℕ) : ((Polynomial.monomial n) a).leadingCoeff = a

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

theorem Polynomial.leadingCoeff_C_mul_X {R : Type u} [Semiring R] (a : R) : (Polynomial.C a * Polynomial.X).leadingCoeff = a

@[simp]

theorem Polynomial.leadingCoeff_C {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).leadingCoeff = a

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

theorem Polynomial.leadingCoeff_X {R : Type u} [Semiring R] : Polynomial.X.leadingCoeff = 1

@[simp]

theorem Polynomial.monic_X_pow {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).Monic

@[simp]

theorem Polynomial.monic_X {R : Type u} [Semiring R] : Polynomial.X.Monic

theorem Polynomial.leadingCoeff_one {R : Type u} [Semiring R] : Polynomial.leadingCoeff 1 = 1

@[simp]

theorem Polynomial.monic_one {R : Type u} [Semiring R] : Polynomial.Monic 1

theorem Polynomial.Monic.ne_zero {R : Type u_2} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p.Monic) : p ≠ 0

theorem Polynomial.Monic.ne_zero_of_ne {R : Type u} [Semiring R] (h : 0 ≠ 1) {p : Polynomial R} (hp : p.Monic) : p ≠ 0

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_of_coeff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.degree ≤ ↑n) (p1 : p.coeff n = 1) : p.Monic

theorem Polynomial.Monic.ne_zero_of_polynomial_ne {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {r : Polynomial R} (hp : p.Monic) (hne : q ≠ r) : p ≠ 0

theorem Polynomial.leadingCoeff_add_of_degree_lt {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R) (q : Polynomial R) : (p * q).coeff (p.natDegree + q.natDegree) = p.leadingCoeff * q.leadingCoeff

theorem Polynomial.degree_mul' {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (hq : q.Monic) : (p * q).degree = p.degree + q.degree

theorem Polynomial.natDegree_mul' {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : (Polynomial.monomial p.natDegree) p.leadingCoeff = p

theorem Polynomial.C_mul_X_pow_eq_self {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p

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 : Polynomial R} {q : Polynomial R} (hp : p.Monic) : (p * q).leadingCoeff = q.leadingCoeff

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

@[simp]

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

@[simp]

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

theorem Polynomial.natDegree_mul_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} : (p * q).natDegree ≤ p.natDegree + q.natDegree

theorem Polynomial.natDegree_mul_le_of_le {R : Type u} {n : ℕ} {m : ℕ} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.natDegree ≤ m) (hg : q.natDegree ≤ n) : (p * q).natDegree ≤ m + n

theorem Polynomial.natDegree_pow_le {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : (p ^ n).natDegree ≤ n * p.natDegree

theorem Polynomial.natDegree_pow_le_of_le {R : Type u} {m : ℕ} [Semiring R] {p : Polynomial R} (n : ℕ) (hp : p.natDegree ≤ m) : (p ^ n).natDegree ≤ n * m

@[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 : Polynomial R} {g : Polynomial R} (hdf : f.natDegree ≤ df) (hdg : g.natDegree ≤ dg) : (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

theorem Polynomial.zero_le_degree_iff {R : Type u} [Semiring R] {p : Polynomial R} : 0 ≤ p.degree ↔ p ≠ 0

theorem Polynomial.natDegree_eq_zero_iff_degree_le_zero {R : Type u} [Semiring R] {p : Polynomial R} : p.natDegree = 0 ↔ p.degree ≤ 0

theorem Polynomial.degree_zero_le {R : Type u} [Semiring R] : Polynomial.degree 0 ≤ 0

theorem Polynomial.degree_le_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : WithBot ℕ) : f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0

theorem Polynomial.degree_lt_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : ℕ) : f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0

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

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

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

theorem Polynomial.natDegree_pos_iff_degree_pos {R : Type u} [Semiring R] {p : Polynomial R} : 0 < p.natDegree ↔ 0 < p.degree

theorem Polynomial.eq_C_of_natDegree_le_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 0) : p = Polynomial.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 = Polynomial.C (p.coeff 0)

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

theorem Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} : p = Polynomial.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

theorem Polynomial.ne_zero_of_coe_le_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) : p ≠ 0

theorem Polynomial.le_natDegree_of_coe_le_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) : n ≤ p.natDegree

theorem Polynomial.degree_sum_fin_lt {R : Type u} [Semiring R] {n : ℕ} (f : Fin n → R) : (Finset.univ.sum fun (i : Fin n) => Polynomial.C (f i) * Polynomial.X ^ ↑i).degree < ↑n

theorem Polynomial.degree_linear_le {R : Type u} {a : R} {b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1

theorem Polynomial.degree_linear_lt {R : Type u} {a : R} {b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree < 2

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

@[simp]

theorem Polynomial.degree_linear {R : Type u} {a : R} {b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree = 1

theorem Polynomial.natDegree_linear_le {R : Type u} {a : R} {b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree ≤ 1

theorem Polynomial.natDegree_linear {R : Type u} {a : R} {b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree = 1

@[simp]

theorem Polynomial.leadingCoeff_linear {R : Type u} {a : R} {b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).leadingCoeff = a

theorem Polynomial.degree_quadratic_le {R : Type u} {a : R} {b : R} {c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree ≤ 2

theorem Polynomial.degree_quadratic_lt {R : Type u} {a : R} {b : R} {c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree < 3

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

@[simp]

theorem Polynomial.degree_quadratic {R : Type u} {a : R} {b : R} {c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree = 2

theorem Polynomial.natDegree_quadratic_le {R : Type u} {a : R} {b : R} {c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree ≤ 2

theorem Polynomial.natDegree_quadratic {R : Type u} {a : R} {b : R} {c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree = 2

@[simp]

theorem Polynomial.leadingCoeff_quadratic {R : Type u} {a : R} {b : R} {c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).leadingCoeff = a

theorem Polynomial.degree_cubic_le {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree ≤ 3

theorem Polynomial.degree_cubic_lt {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < 4

theorem Polynomial.degree_quadratic_lt_degree_C_mul_X_cb {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < (Polynomial.C a * Polynomial.X ^ 3).degree

@[simp]

theorem Polynomial.degree_cubic {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree = 3

theorem Polynomial.natDegree_cubic_le {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree ≤ 3

theorem Polynomial.natDegree_cubic {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree = 3

@[simp]

theorem Polynomial.leadingCoeff_cubic {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).leadingCoeff = a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.natDegree_X_mul {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p ≠ 0) : (Polynomial.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 * Polynomial.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) : (Polynomial.X ^ n * p).natDegree = p.natDegree + n

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

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

@[simp]

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

@[simp]

theorem Polynomial.degree_mul_X_pow {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) : (p * Polynomial.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 - Polynomial.C a).degree = p.degree

@[simp]

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

theorem Polynomial.degree_sub_le {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) : (p - q).degree ≤ max p.degree q.degree

theorem Polynomial.degree_sub_le_of_le {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} {a : WithBot ℕ} {b : WithBot ℕ} (hp : p.degree ≤ a) (hq : q.degree ≤ b) : (p - q).degree ≤ max a b

theorem Polynomial.leadingCoeff_sub_of_degree_lt {R : Type u} [Ring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (h : p.degree = q.degree) (hlc : p.leadingCoeff ≠ q.leadingCoeff) : (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

theorem Polynomial.natDegree_sub_le {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) : (p - q).natDegree ≤ max p.natDegree q.natDegree

theorem Polynomial.natDegree_sub_le_of_le {R : Type u} {n : ℕ} {m : ℕ} [Ring R] {p : Polynomial R} {q : Polynomial R} (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ n) : (p - q).natDegree ≤ max m n

theorem Polynomial.degree_sub_lt {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} (hd : p.degree = q.degree) (hp0 : p ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) : (p - q).degree < p.degree

theorem Polynomial.degree_X_sub_C_le {R : Type u} [Ring R] (r : R) : (Polynomial.X - Polynomial.C r).degree ≤ 1

theorem Polynomial.natDegree_X_sub_C_le {R : Type u} [Ring R] (r : R) : (Polynomial.X - Polynomial.C r).natDegree ≤ 1

theorem Polynomial.degree_sub_eq_left_of_degree_lt {R : Type u} [Ring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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) : (Polynomial.X + Polynomial.C a).degree = 1

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

@[simp]

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

theorem Polynomial.degree_X_pow_add_C {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} (hn : 0 < n) (a : R) : (Polynomial.X ^ n + Polynomial.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) : Polynomial.X ^ n + Polynomial.C a ≠ 0

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

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

theorem Polynomial.natDegree_X_pow_add_C {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} {r : R} : (Polynomial.X ^ n + Polynomial.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) : Polynomial.X ^ n + Polynomial.C a ≠ 1

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem Polynomial.degree_X_pow_sub_C {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} (hn : 0 < n) (a : R) : (Polynomial.X ^ n - Polynomial.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) : Polynomial.X ^ n - Polynomial.C a ≠ 0

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

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

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

@[simp]

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

@[simp]

theorem Polynomial.degree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {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.

Equations

• Polynomial.degreeMonoidHom = { toFun := Polynomial.degree, map_one' := ⋯, map_mul' := ⋯ }

@[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 : Polynomial R) (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

Equations

• Polynomial.leadingCoeffHom = { toFun := Polynomial.leadingCoeff, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Polynomial.leadingCoeffHom_apply {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) : Polynomial.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 : Polynomial R} {p : Polynomial R} (hap : a ∣ p) : a.leadingCoeff ∣ p.leadingCoeff