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

• Polynomial.degree p = Finset.max (Polynomial.support p)

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

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

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

Equations

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

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

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

Equations

• Polynomial.natDegree p = WithBot.unbot' 0 (Polynomial.degree p)

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

• Polynomial.leadingCoeff p = Polynomial.coeff p (Polynomial.natDegree p)

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

a polynomial is Monic if its leading coefficient is 1

Equations

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

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

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

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

Equations

• Polynomial.Monic.decidable = id inferInstance

@[simp]

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

theorem Polynomial.Monic.coeff_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) : Polynomial.coeff p (Polynomial.natDegree p) = 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} : Polynomial.coeff p (Polynomial.natDegree p) = Polynomial.leadingCoeff p

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

theorem Polynomial.degree_mono {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : Polynomial R} {g : Polynomial S} (h : Polynomial.support f ⊆ Polynomial.support g) : Polynomial.degree f ≤ Polynomial.degree g

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

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

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

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

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

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

Alias of the forward direction of Polynomial.natDegree_le_iff_degree_le.

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

Alias of the reverse 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 : Polynomial.degree p ≤ Polynomial.degree q) : Polynomial.natDegree p ≤ Polynomial.natDegree q

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

@[simp]

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

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

theorem Polynomial.degree_C_lt {R : Type u} {a : R} [Semiring R] : Polynomial.degree (Polynomial.C a) < 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.natDegree (Polynomial.C a) = 0

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

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

theorem Polynomial.as_sum_support {R : Type u} [Semiring R] (p : Polynomial R) : p = Finset.sum (Polynomial.support p) fun (i : ℕ) => (Polynomial.monomial i) (Polynomial.coeff p i)

theorem Polynomial.as_sum_support_C_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) : p = Finset.sum (Polynomial.support p) fun (i : ℕ) => Polynomial.C (Polynomial.coeff p 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 : Polynomial.natDegree p < n) : Polynomial.sum p f = Finset.sum (Finset.range n) fun (a : ℕ) => f a (Polynomial.coeff p 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) : Polynomial.sum p f = Finset.sum (Finset.range (Polynomial.natDegree p + 1)) fun (a : ℕ) => f a (Polynomial.coeff p 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 : Polynomial.degree p < ↑n) : (Finset.sum Finset.univ fun (i : Fin n) => f (↑i) (Polynomial.coeff p ↑i)) = Polynomial.sum p f

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

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

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

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

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

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

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

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

theorem Polynomial.exists_eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.natDegree p ≤ 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.degree (Polynomial.X ^ n) ≤ ↑n

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

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

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

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

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

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

theorem Polynomial.nonempty_support_iff {R : Type u} [Semiring R] {p : Polynomial R} : (Polynomial.support p).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.degree Polynomial.X = 1

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

The second-highest coefficient, or 0 for constants

Equations

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Polynomial.natDegree_add_le_of_le {R : Type u} {n : ℕ} {m : ℕ} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.natDegree p ≤ m) (hq : Polynomial.natDegree q ≤ n) : Polynomial.natDegree (p + q) ≤ 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} : Polynomial.leadingCoeff p = 0 ↔ p = 0

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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 : Polynomial.Monic p) : p ≠ 0

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

theorem Polynomial.coeff_mul_add_eq_of_natDegree_le {R : Type u} [Semiring R] {f : Polynomial R} {df : ℕ} {dg : ℕ} {g : Polynomial R} (hdf : Polynomial.natDegree f ≤ df) (hdg : Polynomial.natDegree g ≤ dg) : Polynomial.coeff (f * g) (df + dg) = Polynomial.coeff f df * Polynomial.coeff g dg

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

theorem Polynomial.natDegree_eq_zero_iff_degree_le_zero {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.natDegree p = 0 ↔ Polynomial.degree p ≤ 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 ℕ) : Polynomial.degree f ≤ n ↔ ∀ (m : ℕ), n < ↑m → Polynomial.coeff f m = 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

theorem Polynomial.degree_quadratic_lt {R : Type u} {a : R} {b : R} {c : R} [Semiring R] : Polynomial.degree (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) < 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.degree (Polynomial.C b * Polynomial.X + Polynomial.C c) < Polynomial.degree (Polynomial.C a * Polynomial.X ^ 2)

@[simp]

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

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

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

@[simp]

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

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

theorem Polynomial.degree_cubic_lt {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] : Polynomial.degree (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) < 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.degree (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) < Polynomial.degree (Polynomial.C a * Polynomial.X ^ 3)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Polynomial.natDegree_X_pow_le {R : Type u_1} [Semiring R] (n : ℕ) : Polynomial.natDegree (Polynomial.X ^ n) ≤ 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} : Polynomial.degree (p * Polynomial.X) = Polynomial.degree p + 1

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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 = { toOneHom := { 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 : ℕ) : Polynomial.degree (p ^ n) = n • Polynomial.degree p

@[simp]

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

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 = { toOneHom := { 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 = Polynomial.leadingCoeff p

@[simp]

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

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