# 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} [] (p : ) :

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
Instances For
theorem Polynomial.supDegree_eq_degree {R : Type u} [] (p : ) :
theorem Polynomial.degree_lt_wf {R : Type u} [] :
WellFounded fun (p q : ) => p.degree < q.degree
Equations
• Polynomial.instWellFoundedRelation = { rel := fun (p q : ) => p.degree < q.degree, wf := }
def Polynomial.natDegree {R : Type u} [] (p : ) :

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

Equations
Instances For
def Polynomial.leadingCoeff {R : Type u} [] (p : ) :
R

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

Equations
Instances For
def Polynomial.Monic {R : Type u} [] (p : ) :

a polynomial is Monic if its leading coefficient is 1

Equations
• p.Monic = (p.leadingCoeff = 1)
Instances For
theorem Polynomial.monic_of_subsingleton {R : Type u} [] [] (p : ) :
p.Monic
theorem Polynomial.Monic.def {R : Type u} [] {p : } :
instance Polynomial.Monic.decidable {R : Type u} [] {p : } [] :
Decidable p.Monic
Equations
• Polynomial.Monic.decidable = id inferInstance
@[simp]
theorem Polynomial.Monic.leadingCoeff {R : Type u} [] {p : } (hp : p.Monic) :
theorem Polynomial.Monic.coeff_natDegree {R : Type u} [] {p : } (hp : p.Monic) :
p.coeff p.natDegree = 1
@[simp]
theorem Polynomial.degree_zero {R : Type u} [] :
@[simp]
theorem Polynomial.natDegree_zero {R : Type u} [] :
@[simp]
theorem Polynomial.coeff_natDegree {R : Type u} [] {p : } :
@[simp]
theorem Polynomial.degree_eq_bot {R : Type u} [] {p : } :
p.degree = p = 0
theorem Polynomial.degree_ne_bot {R : Type u} [] {p : } :
p.degree p 0
theorem Polynomial.degree_of_subsingleton {R : Type u} [] {p : } [] :
p.degree =
theorem Polynomial.natDegree_of_subsingleton {R : Type u} [] {p : } [] :
p.natDegree = 0
theorem Polynomial.degree_eq_natDegree {R : Type u} [] {p : } (hp : p 0) :
p.degree = p.natDegree
theorem Polynomial.supDegree_eq_natDegree {R : Type u} [] (p : ) :
theorem Polynomial.degree_eq_iff_natDegree_eq {R : Type u} [] {p : } {n : } (hp : p 0) :
p.degree = n p.natDegree = n
theorem Polynomial.degree_eq_iff_natDegree_eq_of_pos {R : Type u} [] {p : } {n : } (hn : 0 < n) :
p.degree = n p.natDegree = n
theorem Polynomial.natDegree_eq_of_degree_eq_some {R : Type u} [] {p : } {n : } (h : p.degree = n) :
p.natDegree = n
theorem Polynomial.degree_ne_of_natDegree_ne {R : Type u} [] {p : } {n : } :
p.natDegree np.degree n
@[simp]
theorem Polynomial.degree_le_natDegree {R : Type u} [] {p : } :
p.degree p.natDegree
theorem Polynomial.natDegree_eq_of_degree_eq {R : Type u} {S : Type v} [] {p : } [] {q : } (h : p.degree = q.degree) :
p.natDegree = q.natDegree
theorem Polynomial.le_degree_of_ne_zero {R : Type u} {n : } [] {p : } (h : p.coeff n 0) :
n p.degree
theorem Polynomial.le_natDegree_of_ne_zero {R : Type u} {n : } [] {p : } (h : p.coeff n 0) :
n p.natDegree
theorem Polynomial.le_natDegree_of_mem_supp {R : Type u} [] {p : } (a : ) :
a p.supporta p.natDegree
theorem Polynomial.degree_eq_of_le_of_coeff_ne_zero {R : Type u} {n : } [] {p : } (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 : } [] {p : } (pn : p.natDegree n) (p1 : p.coeff n 0) :
p.natDegree = n
theorem Polynomial.degree_mono {R : Type u} {S : Type v} [] [] {f : } {g : } (h : f.support g.support) :
f.degree g.degree
theorem Polynomial.supp_subset_range {R : Type u} {m : } [] {p : } (h : p.natDegree < m) :
p.support
theorem Polynomial.supp_subset_range_natDegree_succ {R : Type u} [] {p : } :
p.support Finset.range (p.natDegree + 1)
theorem Polynomial.degree_le_degree {R : Type u} [] {p : } {q : } (h : q.coeff p.natDegree 0) :
p.degree q.degree
theorem Polynomial.natDegree_le_iff_degree_le {R : Type u} [] {p : } {n : } :
p.natDegree n p.degree n
theorem Polynomial.natDegree_lt_iff_degree_lt {R : Type u} {n : } [] {p : } (hp : p 0) :
p.natDegree < n p.degree < n
theorem Polynomial.natDegree_le_of_degree_le {R : Type u} [] {p : } {n : } :
p.degree np.natDegree n

Alias of the reverse direction of Polynomial.natDegree_le_iff_degree_le.

theorem Polynomial.degree_le_of_natDegree_le {R : Type u} [] {p : } {n : } :
p.natDegree np.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} [] {p : } [] {q : } (hpq : p.degree q.degree) :
p.natDegree q.natDegree
theorem Polynomial.natDegree_lt_natDegree {R : Type u} [] {p : } {q : } (hp : p 0) (hpq : p.degree < q.degree) :
p.natDegree < q.natDegree
@[simp]
theorem Polynomial.degree_C {R : Type u} {a : R} [] (ha : a 0) :
(Polynomial.C a).degree = 0
theorem Polynomial.degree_C_le {R : Type u} {a : R} [] :
(Polynomial.C a).degree 0
theorem Polynomial.degree_C_lt {R : Type u} {a : R} [] :
(Polynomial.C a).degree < 1
@[simp]
theorem Polynomial.natDegree_C {R : Type u} [] (a : R) :
(Polynomial.C a).natDegree = 0
@[simp]
theorem Polynomial.natDegree_one {R : Type u} [] :
@[simp]
theorem Polynomial.natDegree_natCast {R : Type u} [] (n : ) :
(n).natDegree = 0
@[deprecated Polynomial.natDegree_natCast]
theorem Polynomial.natDegree_nat_cast {R : Type u} [] (n : ) :
(n).natDegree = 0

Alias of Polynomial.natDegree_natCast.

theorem Polynomial.degree_natCast_le {R : Type u} [] (n : ) :
(n).degree 0
@[deprecated Polynomial.degree_natCast_le]
theorem Polynomial.degree_nat_cast_le {R : Type u} [] (n : ) :
(n).degree 0

Alias of Polynomial.degree_natCast_le.

@[simp]
theorem Polynomial.degree_monomial {R : Type u} {a : R} [] (n : ) (ha : a 0) :
( a).degree = n
@[simp]
theorem Polynomial.degree_C_mul_X_pow {R : Type u} {a : R} [] (n : ) (ha : a 0) :
(Polynomial.C a * Polynomial.X ^ n).degree = n
theorem Polynomial.degree_C_mul_X {R : Type u} {a : R} [] (ha : a 0) :
(Polynomial.C a * Polynomial.X).degree = 1
theorem Polynomial.degree_monomial_le {R : Type u} [] (n : ) (a : R) :
( a).degree n
theorem Polynomial.degree_C_mul_X_pow_le {R : Type u} [] (n : ) (a : R) :
(Polynomial.C a * Polynomial.X ^ n).degree n
theorem Polynomial.degree_C_mul_X_le {R : Type u} [] (a : R) :
(Polynomial.C a * Polynomial.X).degree 1
@[simp]
theorem Polynomial.natDegree_C_mul_X_pow {R : Type u} [] (n : ) (a : R) (ha : a 0) :
(Polynomial.C a * Polynomial.X ^ n).natDegree = n
@[simp]
theorem Polynomial.natDegree_C_mul_X {R : Type u} [] (a : R) (ha : a 0) :
(Polynomial.C a * Polynomial.X).natDegree = 1
@[simp]
theorem Polynomial.natDegree_monomial {R : Type u} [] [] (i : ) (r : R) :
( r).natDegree = if r = 0 then 0 else i
theorem Polynomial.natDegree_monomial_le {R : Type u} [] (a : R) {m : } :
( a).natDegree m
theorem Polynomial.natDegree_monomial_eq {R : Type u} [] (i : ) {r : R} (r0 : r 0) :
( r).natDegree = i
theorem Polynomial.coeff_eq_zero_of_degree_lt {R : Type u} {n : } [] {p : } (h : p.degree < n) :
p.coeff n = 0
theorem Polynomial.coeff_eq_zero_of_natDegree_lt {R : Type u} [] {p : } {n : } (h : p.natDegree < n) :
p.coeff n = 0
theorem Polynomial.ext_iff_natDegree_le {R : Type u} [] {p : } {q : } {n : } (hp : p.natDegree n) (hq : q.natDegree n) :
p = q in, p.coeff i = q.coeff i
theorem Polynomial.ext_iff_degree_le {R : Type u} [] {p : } {q : } {n : } (hp : p.degree n) (hq : q.degree n) :
p = q in, p.coeff i = q.coeff i
@[simp]
theorem Polynomial.coeff_natDegree_succ_eq_zero {R : Type u} [] {p : } :
p.coeff (p.natDegree + 1) = 0
theorem Polynomial.ite_le_natDegree_coeff {R : Type u} [] (p : ) (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} [] (p : ) :
p = ip.support, (p.coeff i)
theorem Polynomial.as_sum_support_C_mul_X_pow {R : Type u} [] (p : ) :
p = ip.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i
theorem Polynomial.sum_over_range' {R : Type u} {S : Type v} [] [] (p : ) {f : RS} (h : ∀ (n : ), f n 0 = 0) (n : ) (w : p.natDegree < n) :
p.sum f = 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} [] [] (p : ) {f : RS} (h : ∀ (n : ), f n 0 = 0) :
p.sum f = aFinset.range (p.natDegree + 1), 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} [] [] (f : RS) (hf : ∀ (i : ), f i 0 = 0) {n : } {p : } (hn : p.degree < n) :
i : Fin n, f (i) (p.coeff i) = p.sum f
theorem Polynomial.as_sum_range' {R : Type u} [] (p : ) (n : ) (w : p.natDegree < n) :
p = i, (p.coeff i)
theorem Polynomial.as_sum_range {R : Type u} [] (p : ) :
p = iFinset.range (p.natDegree + 1), (p.coeff i)
theorem Polynomial.as_sum_range_C_mul_X_pow {R : Type u} [] (p : ) :
p = iFinset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i
theorem Polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : } [] {p : } (hn : p.degree = n) :
p.coeff n 0
theorem Polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [] {p : } (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} [] {p : } (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} [] {p : } (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} [] {p : } (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} [] {p : } (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} [] (n : ) :
(Polynomial.X ^ n).degree n
theorem Polynomial.degree_X_le {R : Type u} [] :
Polynomial.X.degree 1
theorem Polynomial.natDegree_X_le {R : Type u} [] :
Polynomial.X.natDegree 1
theorem Polynomial.mem_support_C_mul_X_pow {R : Type u} [] {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} [] {c : R} {n : } :
(Polynomial.C c * Polynomial.X ^ n).support.card 1
theorem Polynomial.card_supp_le_succ_natDegree {R : Type u} [] (p : ) :
p.support.card p.natDegree + 1
theorem Polynomial.le_degree_of_mem_supp {R : Type u} [] {p : } (a : ) :
a p.supporta p.degree
theorem Polynomial.nonempty_support_iff {R : Type u} [] {p : } :
p.support.Nonempty p 0
@[simp]
theorem Polynomial.degree_one {R : Type u} [] [] :
@[simp]
theorem Polynomial.degree_X {R : Type u} [] [] :
Polynomial.X.degree = 1
@[simp]
theorem Polynomial.natDegree_X {R : Type u} [] [] :
Polynomial.X.natDegree = 1
theorem Polynomial.coeff_mul_X_sub_C {R : Type u} [Ring R] {p : } {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 : ) :
(-p).degree = p.degree
theorem Polynomial.degree_neg_le_of_le {R : Type u} [Ring R] {a : } {p : } (hp : p.degree a) :
(-p).degree a
@[simp]
theorem Polynomial.natDegree_neg {R : Type u} [Ring R] (p : ) :
(-p).natDegree = p.natDegree
theorem Polynomial.natDegree_neg_le_of_le {R : Type u} {m : } [Ring R] {p : } (hp : p.natDegree m) :
(-p).natDegree m
@[simp]
theorem Polynomial.natDegree_intCast {R : Type u} [Ring R] (n : ) :
(n).natDegree = 0
@[deprecated Polynomial.natDegree_intCast]
theorem Polynomial.natDegree_int_cast {R : Type u} [Ring R] (n : ) :
(n).natDegree = 0

Alias of Polynomial.natDegree_intCast.

theorem Polynomial.degree_intCast_le {R : Type u} [Ring R] (n : ) :
(n).degree 0
@[deprecated Polynomial.degree_intCast_le]
theorem Polynomial.degree_int_cast_le {R : Type u} [Ring R] (n : ) :
(n).degree 0

Alias of Polynomial.degree_intCast_le.

@[simp]
theorem Polynomial.leadingCoeff_neg {R : Type u} [Ring R] (p : ) :
def Polynomial.nextCoeff {R : Type u} [] (p : ) :
R

The second-highest coefficient, or 0 for constants

Equations
• p.nextCoeff = if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)
Instances For
theorem Polynomial.nextCoeff_eq_zero {R : Type u} [] {p : } :
p.nextCoeff = 0 p.natDegree = 0 0 < p.natDegree p.coeff (p.natDegree - 1) = 0
theorem Polynomial.nextCoeff_ne_zero {R : Type u} [] {p : } :
p.nextCoeff 0 p.natDegree 0 p.coeff (p.natDegree - 1) 0
@[simp]
theorem Polynomial.nextCoeff_C_eq_zero {R : Type u} [] (c : R) :
(Polynomial.C c).nextCoeff = 0
theorem Polynomial.nextCoeff_of_natDegree_pos {R : Type u} [] {p : } (hp : 0 < p.natDegree) :
p.nextCoeff = p.coeff (p.natDegree - 1)
theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt {R : Type u} [] {p : } {q : } (h : p.degree < q.degree) :
p.coeff q.natDegree = 0
theorem Polynomial.ne_zero_of_degree_gt {R : Type u} [] {p : } {n : } (h : n < p.degree) :
p 0
theorem Polynomial.ne_zero_of_degree_ge_degree {R : Type u} [] {p : } {q : } (hpq : p.degree q.degree) (hp : p 0) :
q 0
theorem Polynomial.ne_zero_of_natDegree_gt {R : Type u} [] {p : } {n : } (h : n < p.natDegree) :
p 0
theorem Polynomial.degree_lt_degree {R : Type u} [] {p : } {q : } (h : p.natDegree < q.natDegree) :
p.degree < q.degree
theorem Polynomial.natDegree_lt_natDegree_iff {R : Type u} [] {p : } {q : } (hp : p 0) :
p.natDegree < q.natDegree p.degree < q.degree
theorem Polynomial.eq_C_of_degree_le_zero {R : Type u} [] {p : } (h : p.degree 0) :
p = Polynomial.C (p.coeff 0)
theorem Polynomial.eq_C_of_degree_eq_zero {R : Type u} [] {p : } (h : p.degree = 0) :
p = Polynomial.C (p.coeff 0)
theorem Polynomial.degree_le_zero_iff {R : Type u} [] {p : } :
p.degree 0 p = Polynomial.C (p.coeff 0)
theorem Polynomial.degree_add_le {R : Type u} [] (p : ) (q : ) :
(p + q).degree max p.degree q.degree
theorem Polynomial.degree_add_le_of_degree_le {R : Type u} [] {p : } {q : } {n : } (hp : p.degree n) (hq : q.degree n) :
(p + q).degree n
theorem Polynomial.degree_add_le_of_le {R : Type u} [] {p : } {q : } {a : } {b : } (hp : p.degree a) (hq : q.degree b) :
(p + q).degree max a b
theorem Polynomial.natDegree_add_le {R : Type u} [] (p : ) (q : ) :
(p + q).natDegree max p.natDegree q.natDegree
theorem Polynomial.natDegree_add_le_of_degree_le {R : Type u} [] {p : } {q : } {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 : } [] {p : } {q : } (hp : p.natDegree m) (hq : q.natDegree n) :
(p + q).natDegree max m n
@[simp]
theorem Polynomial.leadingCoeff_zero {R : Type u} [] :
@[simp]
theorem Polynomial.leadingCoeff_eq_zero {R : Type u} [] {p : } :
p.leadingCoeff = 0 p = 0
theorem Polynomial.leadingCoeff_ne_zero {R : Type u} [] {p : } :
theorem Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot {R : Type u} [] {p : } :
theorem Polynomial.natDegree_le_pred {R : Type u} {n : } [] {p : } (hf : p.natDegree n) (hn : p.coeff n = 0) :
p.natDegree n - 1
theorem Polynomial.natDegree_mem_support_of_nonzero {R : Type u} [] {p : } (H : p 0) :
p.natDegree p.support
theorem Polynomial.natDegree_eq_support_max' {R : Type u} [] {p : } (h : p 0) :
p.natDegree = p.support.max'
theorem Polynomial.natDegree_C_mul_X_pow_le {R : Type u} [] (a : R) (n : ) :
(Polynomial.C a * Polynomial.X ^ n).natDegree n
theorem Polynomial.degree_add_eq_left_of_degree_lt {R : Type u} [] {p : } {q : } (h : q.degree < p.degree) :
(p + q).degree = p.degree
theorem Polynomial.degree_add_eq_right_of_degree_lt {R : Type u} [] {p : } {q : } (h : p.degree < q.degree) :
(p + q).degree = q.degree
theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt {R : Type u} [] {p : } {q : } (h : q.natDegree < p.natDegree) :
(p + q).natDegree = p.natDegree
theorem Polynomial.natDegree_add_eq_right_of_natDegree_lt {R : Type u} [] {p : } {q : } (h : p.natDegree < q.natDegree) :
(p + q).natDegree = q.natDegree
theorem Polynomial.degree_add_C {R : Type u} {a : R} [] {p : } (hp : 0 < p.degree) :
(p + Polynomial.C a).degree = p.degree
@[simp]
theorem Polynomial.natDegree_add_C {R : Type u} [] {p : } {a : R} :
(p + Polynomial.C a).natDegree = p.natDegree
@[simp]
theorem Polynomial.natDegree_C_add {R : Type u} [] {p : } {a : R} :
(Polynomial.C a + p).natDegree = p.natDegree
(p + q).degree = max p.degree q.degree
theorem Polynomial.natDegree_eq_of_natDegree_add_lt_left {R : Type u} [] (p : ) (q : ) (H : (p + q).natDegree < p.natDegree) :
p.natDegree = q.natDegree
theorem Polynomial.natDegree_eq_of_natDegree_add_lt_right {R : Type u} [] (p : ) (q : ) (H : (p + q).natDegree < q.natDegree) :
p.natDegree = q.natDegree
theorem Polynomial.natDegree_eq_of_natDegree_add_eq_zero {R : Type u} [] (p : ) (q : ) (H : (p + q).natDegree = 0) :
p.natDegree = q.natDegree
theorem Polynomial.degree_erase_le {R : Type u} [] (p : ) (n : ) :
().degree p.degree
theorem Polynomial.degree_erase_lt {R : Type u} [] {p : } (hp : p 0) :
(Polynomial.erase p.natDegree p).degree < p.degree
theorem Polynomial.degree_update_le {R : Type u} [] (p : ) (n : ) (a : R) :
(p.update n a).degree max p.degree n
theorem Polynomial.degree_sum_le {R : Type u} [] {ι : Type u_1} (s : ) (f : ι) :
(is, f i).degree s.sup fun (b : ι) => (f b).degree
theorem Polynomial.degree_mul_le {R : Type u} [] (p : ) (q : ) :
(p * q).degree p.degree + q.degree
theorem Polynomial.degree_mul_le_of_le {R : Type u} [] {p : } {q : } {a : } {b : } (hp : p.degree a) (hq : q.degree b) :
(p * q).degree a + b
theorem Polynomial.degree_pow_le {R : Type u} [] (p : ) (n : ) :
(p ^ n).degree n p.degree
theorem Polynomial.degree_pow_le_of_le {R : Type u} [] {p : } {a : } (b : ) (hp : p.degree a) :
(p ^ b).degree b * a
@[simp]
theorem Polynomial.leadingCoeff_monomial {R : Type u} [] (a : R) (n : ) :
theorem Polynomial.leadingCoeff_C_mul_X_pow {R : Type u} [] (a : R) (n : ) :
(Polynomial.C a * Polynomial.X ^ n).leadingCoeff = a
theorem Polynomial.leadingCoeff_C_mul_X {R : Type u} [] (a : R) :
(Polynomial.C a * Polynomial.X).leadingCoeff = a
@[simp]
theorem Polynomial.leadingCoeff_C {R : Type u} [] (a : R) :
theorem Polynomial.leadingCoeff_X_pow {R : Type u} [] (n : ) :
theorem Polynomial.leadingCoeff_X {R : Type u} [] :
@[simp]
theorem Polynomial.monic_X_pow {R : Type u} [] (n : ) :
(Polynomial.X ^ n).Monic
@[simp]
theorem Polynomial.monic_X {R : Type u} [] :
Polynomial.X.Monic
@[simp]
theorem Polynomial.monic_one {R : Type u} [] :
theorem Polynomial.Monic.ne_zero {R : Type u_2} [] [] {p : } (hp : p.Monic) :
p 0
theorem Polynomial.Monic.ne_zero_of_ne {R : Type u} [] (h : 0 1) {p : } (hp : p.Monic) :
p 0
theorem Polynomial.monic_of_natDegree_le_of_coeff_eq_one {R : Type u} [] {p : } (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} [] {p : } (n : ) (pn : p.degree n) (p1 : p.coeff n = 1) :
p.Monic
theorem Polynomial.Monic.ne_zero_of_polynomial_ne {R : Type u} [] {p : } {q : } {r : } (hp : p.Monic) (hne : q r) :
p 0
theorem Polynomial.leadingCoeff_add_of_degree_lt {R : Type u} [] {p : } {q : } (h : p.degree < q.degree) :
theorem Polynomial.leadingCoeff_add_of_degree_lt' {R : Type u} [] {p : } {q : } (h : q.degree < p.degree) :
theorem Polynomial.leadingCoeff_add_of_degree_eq {R : Type u} [] {p : } {q : } (h : p.degree = q.degree) (hlc : p.leadingCoeff + q.leadingCoeff 0) :
@[simp]
theorem Polynomial.coeff_mul_degree_add_degree {R : Type u} [] (p : ) (q : ) :
theorem Polynomial.degree_mul' {R : Type u} [] {p : } {q : } (h : p.leadingCoeff * q.leadingCoeff 0) :
(p * q).degree = p.degree + q.degree
theorem Polynomial.Monic.degree_mul {R : Type u} [] {p : } {q : } (hq : q.Monic) :
(p * q).degree = p.degree + q.degree
theorem Polynomial.natDegree_mul' {R : Type u} [] {p : } {q : } (h : p.leadingCoeff * q.leadingCoeff 0) :
(p * q).natDegree = p.natDegree + q.natDegree
theorem Polynomial.leadingCoeff_mul' {R : Type u} [] {p : } {q : } (h : p.leadingCoeff * q.leadingCoeff 0) :
theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self {R : Type u} [] {p : } (h : p.support.card 1) :
theorem Polynomial.C_mul_X_pow_eq_self {R : Type u} [] {p : } (h : p.support.card 1) :
Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p
theorem Polynomial.leadingCoeff_pow' {R : Type u} {n : } [] {p : } :
theorem Polynomial.degree_pow' {R : Type u} [] {p : } {n : } :
p.leadingCoeff ^ n 0(p ^ n).degree = n p.degree
theorem Polynomial.natDegree_pow' {R : Type u} [] {p : } {n : } (h : p.leadingCoeff ^ n 0) :
(p ^ n).natDegree = n * p.natDegree
theorem Polynomial.leadingCoeff_monic_mul {R : Type u} [] {p : } {q : } (hp : p.Monic) :
theorem Polynomial.leadingCoeff_mul_monic {R : Type u} [] {p : } {q : } (hq : q.Monic) :
@[simp]
theorem Polynomial.leadingCoeff_mul_X_pow {R : Type u} [] {p : } {n : } :
@[simp]
theorem Polynomial.leadingCoeff_mul_X {R : Type u} [] {p : } :
theorem Polynomial.natDegree_mul_le {R : Type u} [] {p : } {q : } :
(p * q).natDegree p.natDegree + q.natDegree
theorem Polynomial.natDegree_mul_le_of_le {R : Type u} {n : } {m : } [] {p : } {q : } (hp : p.natDegree m) (hg : q.natDegree n) :
(p * q).natDegree m + n
theorem Polynomial.natDegree_pow_le {R : Type u} [] {p : } {n : } :
(p ^ n).natDegree n * p.natDegree
theorem Polynomial.natDegree_pow_le_of_le {R : Type u} {m : } [] {p : } (n : ) (hp : p.natDegree m) :
(p ^ n).natDegree n * m
@[simp]
theorem Polynomial.coeff_pow_mul_natDegree {R : Type u} [] (p : ) (n : ) :
(p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n
theorem Polynomial.coeff_mul_add_eq_of_natDegree_le {R : Type u} [] {df : } {dg : } {f : } {g : } (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} [] {p : } :
0 p.degree p 0
theorem Polynomial.natDegree_eq_zero_iff_degree_le_zero {R : Type u} [] {p : } :
p.natDegree = 0 p.degree 0
theorem Polynomial.degree_le_iff_coeff_zero {R : Type u} [] (f : ) (n : ) :
f.degree n ∀ (m : ), n < mf.coeff m = 0
theorem Polynomial.degree_lt_iff_coeff_zero {R : Type u} [] (f : ) (n : ) :
f.degree < n ∀ (m : ), n mf.coeff m = 0
theorem Polynomial.degree_smul_le {R : Type u} [] (a : R) (p : ) :
(a p).degree p.degree
theorem Polynomial.natDegree_smul_le {R : Type u} [] (a : R) (p : ) :
(a p).natDegree p.natDegree
theorem Polynomial.degree_lt_degree_mul_X {R : Type u} [] {p : } (hp : p 0) :
p.degree < (p * Polynomial.X).degree
theorem Polynomial.natDegree_pos_iff_degree_pos {R : Type u} [] {p : } :
0 < p.natDegree 0 < p.degree
theorem Polynomial.eq_C_of_natDegree_le_zero {R : Type u} [] {p : } (h : p.natDegree 0) :
p = Polynomial.C (p.coeff 0)
theorem Polynomial.eq_C_of_natDegree_eq_zero {R : Type u} [] {p : } (h : p.natDegree = 0) :
p = Polynomial.C (p.coeff 0)
theorem Polynomial.natDegree_eq_zero {R : Type u} [] {p : } :
p.natDegree = 0 ∃ (x : R), Polynomial.C x = p
theorem Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero {R : Type u} [] {p : } :
p = Polynomial.C (p.coeff 0) p.natDegree = 0
theorem Polynomial.eq_one_of_monic_natDegree_zero {R : Type u} [] {p : } (hf : p.Monic) (hfd : p.natDegree = 0) :
p = 1
theorem Polynomial.Monic.natDegree_eq_zero {R : Type u} [] {p : } (hf : p.Monic) :
p.natDegree = 0 p = 1
theorem Polynomial.ne_zero_of_coe_le_degree {R : Type u} {n : } [] {p : } (hdeg : n p.degree) :
p 0
theorem Polynomial.le_natDegree_of_coe_le_degree {R : Type u} {n : } [] {p : } (hdeg : n p.degree) :
n p.natDegree
theorem Polynomial.degree_sum_fin_lt {R : Type u} [] {n : } (f : Fin nR) :
(i : Fin n, Polynomial.C (f i) * Polynomial.X ^ i).degree < n
theorem Polynomial.degree_linear_le {R : Type u} {a : R} {b : R} [] :
(Polynomial.C a * Polynomial.X + Polynomial.C b).degree 1
theorem Polynomial.degree_linear_lt {R : Type u} {a : R} {b : 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} [] (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} [] (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} [] :
(Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree 1
theorem Polynomial.natDegree_linear {R : Type u} {a : R} {b : 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} [] (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} [] :
(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} [] :
(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} [] (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} [] (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} [] :
(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} [] (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} [] (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} [] :
(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} [] :
(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} [] (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} [] (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} [] :
(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} [] (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} [] (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} [] [] (n : ) :
(Polynomial.X ^ n).degree = n
@[simp]
theorem Polynomial.natDegree_X_pow {R : Type u} [] [] (n : ) :
(Polynomial.X ^ n).natDegree = n
@[simp]
theorem Polynomial.natDegree_mul_X {R : Type u} [] [] {p : } (hp : p 0) :
(p * Polynomial.X).natDegree = p.natDegree + 1
@[simp]
theorem Polynomial.natDegree_X_mul {R : Type u} [] [] {p : } (hp : p 0) :
(Polynomial.X * p).natDegree = p.natDegree + 1
@[simp]
theorem Polynomial.natDegree_mul_X_pow {R : Type u} [] [] {p : } (n : ) (hp : p 0) :
(p * Polynomial.X ^ n).natDegree = p.natDegree + n
@[simp]
theorem Polynomial.natDegree_X_pow_mul {R : Type u} [] [] {p : } (n : ) (hp : p 0) :
(Polynomial.X ^ n * p).natDegree = p.natDegree + n
theorem Polynomial.natDegree_X_pow_le {R : Type u_1} [] (n : ) :
(Polynomial.X ^ n).natDegree n
theorem Polynomial.not_isUnit_X {R : Type u} [] [] :
¬IsUnit Polynomial.X
@[simp]
theorem Polynomial.degree_mul_X {R : Type u} [] [] {p : } :
(p * Polynomial.X).degree = p.degree + 1
@[simp]
theorem Polynomial.degree_mul_X_pow {R : Type u} [] [] {p : } (n : ) :
(p * Polynomial.X ^ n).degree = p.degree + n
theorem Polynomial.degree_sub_C {R : Type u} {a : R} [Ring R] {p : } (hp : 0 < p.degree) :
(p - Polynomial.C a).degree = p.degree
@[simp]
theorem Polynomial.natDegree_sub_C {R : Type u} [Ring R] {p : } {a : R} :
(p - Polynomial.C a).natDegree = p.natDegree
theorem Polynomial.degree_sub_le {R : Type u} [Ring R] (p : ) (q : ) :
(p - q).degree max p.degree q.degree
theorem Polynomial.degree_sub_le_of_le {R : Type u} [Ring R] {p : } {q : } {a : } {b : } (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 : } {q : } (h : q.degree < p.degree) :
theorem Polynomial.leadingCoeff_sub_of_degree_lt' {R : Type u} [Ring R] {p : } {q : } (h : p.degree < q.degree) :
theorem Polynomial.leadingCoeff_sub_of_degree_eq {R : Type u} [Ring R] {p : } {q : } (h : p.degree = q.degree) (hlc : p.leadingCoeff q.leadingCoeff) :
theorem Polynomial.natDegree_sub_le {R : Type u} [Ring R] (p : ) (q : ) :
(p - q).natDegree max p.natDegree q.natDegree
theorem Polynomial.natDegree_sub_le_of_le {R : Type u} {n : } {m : } [Ring R] {p : } {q : } (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 : } {q : } (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 : } {q : } (h : q.degree < p.degree) :
(p - q).degree = p.degree
theorem Polynomial.degree_sub_eq_right_of_degree_lt {R : Type u} [Ring R] {p : } {q : } (h : p.degree < q.degree) :
(p - q).degree = q.degree
theorem Polynomial.natDegree_sub_eq_left_of_natDegree_lt {R : Type u} [Ring R] {p : } {q : } (h : q.natDegree < p.natDegree) :
(p - q).natDegree = p.natDegree
theorem Polynomial.natDegree_sub_eq_right_of_natDegree_lt {R : Type u} [Ring R] {p : } {q : } (h : p.natDegree < q.natDegree) :
(p - q).natDegree = q.natDegree
@[simp]
theorem Polynomial.degree_X_add_C {R : Type u} [] [] (a : R) :
(Polynomial.X + Polynomial.C a).degree = 1
theorem Polynomial.natDegree_X_add_C {R : Type u} [] [] (x : R) :
(Polynomial.X + Polynomial.C x).natDegree = 1
@[simp]
theorem Polynomial.nextCoeff_X_add_C {S : Type v} [] (c : S) :
(Polynomial.X + Polynomial.C c).nextCoeff = c
theorem Polynomial.degree_X_pow_add_C {R : Type u} [] [] {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} [] [] {n : } (hn : 0 < n) (a : R) :
Polynomial.X ^ n + Polynomial.C a 0
theorem Polynomial.X_add_C_ne_zero {R : Type u} [] [] (r : R) :
Polynomial.X + Polynomial.C r 0
theorem Polynomial.zero_nmem_multiset_map_X_add_C {R : Type u} [] [] {α : Type u_1} (m : ) (f : αR) :
0Multiset.map (fun (a : α) => Polynomial.X + Polynomial.C (f a)) m
theorem Polynomial.natDegree_X_pow_add_C {R : Type u} [] [] {n : } {r : R} :
(Polynomial.X ^ n + Polynomial.C r).natDegree = n
theorem Polynomial.X_pow_add_C_ne_one {R : Type u} [] [] {n : } (hn : 0 < n) (a : R) :
Polynomial.X ^ n + Polynomial.C a 1
theorem Polynomial.X_add_C_ne_one {R : Type u} [] [] (r : R) :
Polynomial.X + Polynomial.C r 1
@[simp]
theorem Polynomial.leadingCoeff_X_pow_add_C {R : Type u} [] {n : } (hn : 0 < n) {r : R} :
(Polynomial.X ^ n + Polynomial.C r).leadingCoeff = 1
@[simp]
(Polynomial.X + Polynomial.C r).leadingCoeff = 1
@[simp]
theorem Polynomial.leadingCoeff_X_pow_add_one {R : Type u} [] {n : } (hn : 0 < n) :
(Polynomial.X ^ n + 1).leadingCoeff = 1
@[simp]
theorem Polynomial.leadingCoeff_pow_X_add_C {R : Type u} [] (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] [] (a : R) :
(Polynomial.X - Polynomial.C a).degree = 1
theorem Polynomial.natDegree_X_sub_C {R : Type u} [Ring 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] [] {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] [] {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] [] (r : R) :
Polynomial.X - Polynomial.C r 0
theorem Polynomial.zero_nmem_multiset_map_X_sub_C {R : Type u} [Ring R] [] {α : Type u_1} (m : ) (f : αR) :
0Multiset.map (fun (a : α) => Polynomial.X - Polynomial.C (f a)) m
theorem Polynomial.natDegree_X_pow_sub_C {R : Type u} [Ring 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} [] [] {p : } {q : } :
(p * q).degree = p.degree + q.degree
def Polynomial.degreeMonoidHom {R : Type u} [] [] [] :

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' := }
Instances For
@[simp]
theorem Polynomial.degree_pow {R : Type u} [] [] [] (p : ) (n : ) :
(p ^ n).degree = n p.degree
@[simp]
theorem Polynomial.leadingCoeff_mul {R : Type u} [] [] (p : ) (q : ) :
def Polynomial.leadingCoeffHom {R : Type u} [] [] :
→* 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' := }
Instances For
@[simp]
theorem Polynomial.leadingCoeffHom_apply {R : Type u} [] [] (p : ) :