# 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
Instances For
theorem Polynomial.supDegree_eq_degree {R : Type u} [] (p : ) :
theorem Polynomial.degree_lt_wf {R : Type u} [] :
WellFounded fun (p q : ) =>
Equations
• One or more equations did not get rendered due to their size.
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
Instances For
theorem Polynomial.monic_of_subsingleton {R : Type u} [] [] (p : ) :
theorem Polynomial.Monic.def {R : Type u} [] {p : } :
instance Polynomial.Monic.decidable {R : Type u} [] {p : } [] :
Equations
• Polynomial.Monic.decidable = id inferInstance
@[simp]
theorem Polynomial.Monic.leadingCoeff {R : Type u} [] {p : } (hp : ) :
theorem Polynomial.Monic.coeff_natDegree {R : Type u} [] {p : } (hp : ) :
@[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 = 0
theorem Polynomial.degree_of_subsingleton {R : Type u} [] {p : } [] :
theorem Polynomial.natDegree_of_subsingleton {R : Type u} [] {p : } [] :
theorem Polynomial.degree_eq_natDegree {R : Type u} [] {p : } (hp : p 0) :
theorem Polynomial.degree_eq_iff_natDegree_eq {R : Type u} [] {p : } {n : } (hp : p 0) :
theorem Polynomial.degree_eq_iff_natDegree_eq_of_pos {R : Type u} [] {p : } {n : } (hn : 0 < n) :
theorem Polynomial.natDegree_eq_of_degree_eq_some {R : Type u} [] {p : } {n : } (h : ) :
theorem Polynomial.degree_ne_of_natDegree_ne {R : Type u} [] {p : } {n : } :
@[simp]
theorem Polynomial.degree_le_natDegree {R : Type u} [] {p : } :
theorem Polynomial.natDegree_eq_of_degree_eq {R : Type u} {S : Type v} [] {p : } [] {q : } (h : ) :
theorem Polynomial.le_degree_of_ne_zero {R : Type u} {n : } [] {p : } (h : 0) :
theorem Polynomial.le_natDegree_of_ne_zero {R : Type u} {n : } [] {p : } (h : 0) :
theorem Polynomial.le_natDegree_of_mem_supp {R : Type u} [] {p : } (a : ) :
theorem Polynomial.degree_eq_of_le_of_coeff_ne_zero {R : Type u} {n : } [] {p : } (pn : ) (p1 : 0) :
theorem Polynomial.natDegree_eq_of_le_of_coeff_ne_zero {R : Type u} {n : } [] {p : } (pn : ) (p1 : 0) :
theorem Polynomial.degree_mono {R : Type u} {S : Type v} [] [] {f : } {g : } (h : ) :
theorem Polynomial.supp_subset_range {R : Type u} {m : } [] {p : } (h : ) :
theorem Polynomial.degree_le_degree {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.natDegree_le_iff_degree_le {R : Type u} [] {p : } {n : } :
theorem Polynomial.natDegree_lt_iff_degree_lt {R : Type u} {n : } [] {p : } (hp : p 0) :
theorem Polynomial.degree_le_of_natDegree_le {R : Type u} [] {p : } {n : } :

Alias of the forward direction of Polynomial.natDegree_le_iff_degree_le.

theorem Polynomial.natDegree_le_of_degree_le {R : Type u} [] {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} [] {p : } [] {q : } (hpq : ) :
theorem Polynomial.natDegree_lt_natDegree {R : Type u} [] {p : } {q : } (hp : p 0) (hpq : ) :
@[simp]
theorem Polynomial.degree_C {R : Type u} {a : R} [] (ha : a 0) :
Polynomial.degree (Polynomial.C a) = 0
theorem Polynomial.degree_C_le {R : Type u} {a : R} [] :
Polynomial.degree (Polynomial.C a) 0
theorem Polynomial.degree_C_lt {R : Type u} {a : R} [] :
Polynomial.degree (Polynomial.C a) < 1
@[simp]
theorem Polynomial.natDegree_C {R : Type u} [] (a : R) :
Polynomial.natDegree (Polynomial.C a) = 0
@[simp]
theorem Polynomial.natDegree_one {R : Type u} [] :
@[simp]
theorem Polynomial.natDegree_nat_cast {R : Type u} [] (n : ) :
theorem Polynomial.degree_nat_cast_le {R : Type u} [] (n : ) :
@[simp]
theorem Polynomial.degree_monomial {R : Type u} {a : R} [] (n : ) (ha : a 0) :
= n
@[simp]
theorem Polynomial.degree_C_mul_X_pow {R : Type u} {a : 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} [] (ha : a 0) :
Polynomial.degree (Polynomial.C a * Polynomial.X) = 1
theorem Polynomial.degree_monomial_le {R : Type u} [] (n : ) (a : R) :
n
theorem Polynomial.degree_C_mul_X_pow_le {R : Type u} [] (n : ) (a : R) :
Polynomial.degree (Polynomial.C a * Polynomial.X ^ n) n
theorem Polynomial.degree_C_mul_X_le {R : Type u} [] (a : R) :
Polynomial.degree (Polynomial.C a * Polynomial.X) 1
@[simp]
theorem Polynomial.natDegree_C_mul_X_pow {R : Type u} [] (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} [] (a : R) (ha : a 0) :
Polynomial.natDegree (Polynomial.C a * Polynomial.X) = 1
@[simp]
theorem Polynomial.natDegree_monomial {R : Type u} [] [] (i : ) (r : R) :
= if r = 0 then 0 else i
theorem Polynomial.natDegree_monomial_le {R : Type u} [] (a : R) {m : } :
m
theorem Polynomial.natDegree_monomial_eq {R : Type u} [] (i : ) {r : R} (r0 : r 0) :
= i
theorem Polynomial.coeff_eq_zero_of_degree_lt {R : Type u} {n : } [] {p : } (h : ) :
= 0
theorem Polynomial.coeff_eq_zero_of_natDegree_lt {R : Type u} [] {p : } {n : } (h : ) :
= 0
theorem Polynomial.ext_iff_natDegree_le {R : Type u} [] {p : } {q : } {n : } (hp : ) (hq : ) :
p = q in,
theorem Polynomial.ext_iff_degree_le {R : Type u} [] {p : } {q : } {n : } (hp : ) (hq : ) :
p = q in,
@[simp]
theorem Polynomial.coeff_natDegree_succ_eq_zero {R : Type u} [] {p : } :
= 0
theorem Polynomial.ite_le_natDegree_coeff {R : Type u} [] (p : ) (n : ) (I : Decidable (n < )) :
(if n < then else 0) =
theorem Polynomial.as_sum_support {R : Type u} [] (p : ) :
p = Finset.sum fun (i : ) => ()
theorem Polynomial.as_sum_support_C_mul_X_pow {R : Type u} [] (p : ) :
p = Finset.sum fun (i : ) => Polynomial.C () * 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 : ) :
= Finset.sum () fun (a : ) => f 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) :
= Finset.sum () fun (a : ) => f 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 : ) :
(Finset.sum Finset.univ fun (i : Fin n) => f (i) ()) =
theorem Polynomial.as_sum_range' {R : Type u} [] (p : ) (n : ) (w : ) :
p = Finset.sum () fun (i : ) => ()
theorem Polynomial.as_sum_range {R : Type u} [] (p : ) :
p = Finset.sum () fun (i : ) => ()
theorem Polynomial.as_sum_range_C_mul_X_pow {R : Type u} [] (p : ) :
p = Finset.sum () fun (i : ) => Polynomial.C () * Polynomial.X ^ i
theorem Polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : } [] {p : } (hn : ) :
0
theorem Polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [] {p : } (h : ) :
p = Polynomial.C () * Polynomial.X + Polynomial.C ()
theorem Polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [] {p : } (h : ) :
p = Polynomial.C * Polynomial.X + Polynomial.C ()
theorem Polynomial.eq_X_add_C_of_natDegree_le_one {R : Type u} [] {p : } (h : ) :
p = Polynomial.C () * Polynomial.X + Polynomial.C ()
theorem Polynomial.Monic.eq_X_add_C {R : Type u} [] {p : } (hm : ) (hnd : ) :
p = Polynomial.X + Polynomial.C ()
theorem Polynomial.exists_eq_X_add_C_of_natDegree_le_one {R : Type u} [] {p : } (h : ) :
∃ (a : R) (b : R), p = Polynomial.C a * Polynomial.X + Polynomial.C b
theorem Polynomial.degree_X_pow_le {R : Type u} [] (n : ) :
Polynomial.degree (Polynomial.X ^ n) n
theorem Polynomial.degree_X_le {R : Type u} [] :
Polynomial.degree Polynomial.X 1
theorem Polynomial.mem_support_C_mul_X_pow {R : Type u} [] {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} [] {c : R} {n : } :
(Polynomial.support (Polynomial.C c * Polynomial.X ^ n)).card 1
theorem Polynomial.card_supp_le_succ_natDegree {R : Type u} [] (p : ) :
.card
theorem Polynomial.le_degree_of_mem_supp {R : Type u} [] {p : } (a : ) :
theorem Polynomial.nonempty_support_iff {R : Type u} [] {p : } :
.Nonempty p 0
@[simp]
theorem Polynomial.degree_one {R : Type u} [] [] :
@[simp]
theorem Polynomial.degree_X {R : Type u} [] [] :
Polynomial.degree Polynomial.X = 1
@[simp]
theorem Polynomial.natDegree_X {R : Type u} [] [] :
Polynomial.natDegree Polynomial.X = 1
theorem Polynomial.coeff_mul_X_sub_C {R : Type u} [Ring R] {p : } {r : R} {a : } :
Polynomial.coeff (p * (Polynomial.X - Polynomial.C r)) (a + 1) = - Polynomial.coeff p (a + 1) * r
@[simp]
theorem Polynomial.degree_neg {R : Type u} [Ring R] (p : ) :
theorem Polynomial.degree_neg_le_of_le {R : Type u} [Ring R] {a : } {p : } (hp : ) :
a
@[simp]
theorem Polynomial.natDegree_neg {R : Type u} [Ring R] (p : ) :
theorem Polynomial.natDegree_neg_le_of_le {R : Type u} {m : } [Ring R] {p : } (hp : ) :
@[simp]
theorem Polynomial.natDegree_int_cast {R : Type u} [Ring R] (n : ) :
theorem Polynomial.degree_int_cast_le {R : Type u} [Ring R] (n : ) :
@[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
• = if then 0 else
Instances For
theorem Polynomial.nextCoeff_eq_zero {R : Type u} [] {p : } :
theorem Polynomial.nextCoeff_ne_zero {R : Type u} [] {p : } :
@[simp]
theorem Polynomial.nextCoeff_C_eq_zero {R : Type u} [] (c : R) :
Polynomial.nextCoeff (Polynomial.C c) = 0
theorem Polynomial.nextCoeff_of_natDegree_pos {R : Type u} [] {p : } (hp : ) :
theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.ne_zero_of_degree_gt {R : Type u} [] {p : } {n : } (h : ) :
p 0
theorem Polynomial.ne_zero_of_degree_ge_degree {R : Type u} [] {p : } {q : } (hpq : ) (hp : p 0) :
q 0
theorem Polynomial.ne_zero_of_natDegree_gt {R : Type u} [] {p : } {n : } (h : ) :
p 0
theorem Polynomial.degree_lt_degree {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.natDegree_lt_natDegree_iff {R : Type u} [] {p : } {q : } (hp : p 0) :
theorem Polynomial.eq_C_of_degree_le_zero {R : Type u} [] {p : } (h : ) :
p = Polynomial.C ()
theorem Polynomial.eq_C_of_degree_eq_zero {R : Type u} [] {p : } (h : ) :
p = Polynomial.C ()
theorem Polynomial.degree_le_zero_iff {R : Type u} [] {p : } :
p = Polynomial.C ()
theorem Polynomial.degree_add_le {R : Type u} [] (p : ) (q : ) :
theorem Polynomial.degree_add_le_of_degree_le {R : Type u} [] {p : } {q : } {n : } (hp : ) (hq : ) :
theorem Polynomial.degree_add_le_of_le {R : Type u} [] {p : } {q : } {a : } {b : } (hp : ) (hq : ) :
theorem Polynomial.natDegree_add_le {R : Type u} [] (p : ) (q : ) :
theorem Polynomial.natDegree_add_le_of_degree_le {R : Type u} [] {p : } {q : } {n : } (hp : ) (hq : ) :
theorem Polynomial.natDegree_add_le_of_le {R : Type u} {n : } {m : } [] {p : } {q : } (hp : ) (hq : ) :
@[simp]
theorem Polynomial.leadingCoeff_zero {R : Type u} [] :
@[simp]
theorem Polynomial.leadingCoeff_eq_zero {R : Type u} [] {p : } :
p = 0
theorem Polynomial.leadingCoeff_ne_zero {R : Type u} [] {p : } :
p 0
theorem Polynomial.natDegree_le_pred {R : Type u} {n : } [] {p : } (hf : ) (hn : = 0) :
n - 1
theorem Polynomial.natDegree_mem_support_of_nonzero {R : Type u} [] {p : } (H : p 0) :
theorem Polynomial.natDegree_eq_support_max' {R : Type u} [] {p : } (h : p 0) :
= Finset.max' (_ : .Nonempty)
theorem Polynomial.natDegree_C_mul_X_pow_le {R : Type u} [] (a : R) (n : ) :
Polynomial.natDegree (Polynomial.C a * Polynomial.X ^ n) n
theorem Polynomial.degree_add_eq_left_of_degree_lt {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.degree_add_eq_right_of_degree_lt {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.natDegree_add_eq_right_of_natDegree_lt {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.degree_add_C {R : Type u} {a : R} [] {p : } (hp : ) :
Polynomial.degree (p + Polynomial.C a) =
@[simp]
theorem Polynomial.natDegree_add_C {R : Type u} [] {p : } {a : R} :
Polynomial.natDegree (p + Polynomial.C a) =
@[simp]
theorem Polynomial.natDegree_C_add {R : Type u} [] {p : } {a : R} :
Polynomial.natDegree (Polynomial.C a + p) =
theorem Polynomial.natDegree_eq_of_natDegree_add_lt_left {R : Type u} [] (p : ) (q : ) (H : ) :
theorem Polynomial.natDegree_eq_of_natDegree_add_lt_right {R : Type u} [] (p : ) (q : ) (H : ) :
theorem Polynomial.degree_erase_le {R : Type u} [] (p : ) (n : ) :
theorem Polynomial.degree_erase_lt {R : Type u} [] {p : } (hp : p 0) :
theorem Polynomial.degree_update_le {R : Type u} [] (p : ) (n : ) (a : R) :
max n
theorem Polynomial.degree_sum_le {R : Type u} [] {ι : Type u_1} (s : ) (f : ι) :
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} [] (p : ) (q : ) :
theorem Polynomial.degree_mul_le_of_le {R : Type u} [] {p : } {q : } {a : } {b : } (hp : ) (hq : ) :
theorem Polynomial.degree_pow_le {R : Type u} [] (p : ) (n : ) :
theorem Polynomial.degree_pow_le_of_le {R : Type u} [] {p : } {a : } (b : ) (hp : ) :
Polynomial.degree (p ^ b) 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.leadingCoeff (Polynomial.C a * Polynomial.X ^ n) = a
theorem Polynomial.leadingCoeff_C_mul_X {R : Type u} [] (a : R) :
Polynomial.leadingCoeff (Polynomial.C a * Polynomial.X) = a
@[simp]
theorem Polynomial.leadingCoeff_C {R : Type u} [] (a : R) :
theorem Polynomial.leadingCoeff_X_pow {R : Type u} [] (n : ) :
Polynomial.leadingCoeff (Polynomial.X ^ n) = 1
@[simp]
theorem Polynomial.monic_X_pow {R : Type u} [] (n : ) :
Polynomial.Monic (Polynomial.X ^ n)
@[simp]
theorem Polynomial.monic_X {R : Type u} [] :
Polynomial.Monic Polynomial.X
@[simp]
theorem Polynomial.monic_one {R : Type u} [] :
theorem Polynomial.Monic.ne_zero {R : Type u_2} [] [] {p : } (hp : ) :
p 0
theorem Polynomial.Monic.ne_zero_of_ne {R : Type u} [] (h : 0 1) {p : } (hp : ) :
p 0
theorem Polynomial.monic_of_natDegree_le_of_coeff_eq_one {R : Type u} [] {p : } (n : ) (pn : ) (p1 : = 1) :
theorem Polynomial.monic_of_degree_le_of_coeff_eq_one {R : Type u} [] {p : } (n : ) (pn : ) (p1 : = 1) :
theorem Polynomial.Monic.ne_zero_of_polynomial_ne {R : Type u} [] {p : } {q : } {r : } (hp : ) (hne : q r) :
p 0
theorem Polynomial.leadingCoeff_add_of_degree_lt {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.leadingCoeff_add_of_degree_lt' {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.leadingCoeff_add_of_degree_eq {R : Type u} [] {p : } {q : } (h : ) (hlc : ) :
@[simp]
theorem Polynomial.coeff_mul_degree_add_degree {R : Type u} [] (p : ) (q : ) :
theorem Polynomial.degree_mul' {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.Monic.degree_mul {R : Type u} [] {p : } {q : } (hq : ) :
theorem Polynomial.natDegree_mul' {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.leadingCoeff_mul' {R : Type u} [] {p : } {q : } (h : ) :
theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self {R : Type u} [] {p : } (h : .card 1) :
theorem Polynomial.C_mul_X_pow_eq_self {R : Type u} [] {p : } (h : .card 1) :
Polynomial.C * Polynomial.X ^ = p
theorem Polynomial.leadingCoeff_pow' {R : Type u} {n : } [] {p : } :
theorem Polynomial.degree_pow' {R : Type u} [] {p : } {n : } :
Polynomial.degree (p ^ n) =
theorem Polynomial.natDegree_pow' {R : Type u} [] {p : } {n : } (h : ) :
theorem Polynomial.leadingCoeff_monic_mul {R : Type u} [] {p : } {q : } (hp : ) :
theorem Polynomial.leadingCoeff_mul_monic {R : Type u} [] {p : } {q : } (hq : ) :
@[simp]
theorem Polynomial.leadingCoeff_mul_X_pow {R : Type u} [] {p : } {n : } :
Polynomial.leadingCoeff (p * Polynomial.X ^ n) =
@[simp]
theorem Polynomial.leadingCoeff_mul_X {R : Type u} [] {p : } :
theorem Polynomial.natDegree_mul_le {R : Type u} [] {p : } {q : } :
theorem Polynomial.natDegree_mul_le_of_le {R : Type u} {n : } {m : } [] {p : } {q : } (hp : ) (hg : ) :
theorem Polynomial.natDegree_pow_le {R : Type u} [] {p : } {n : } :
theorem Polynomial.natDegree_pow_le_of_le {R : Type u} {m : } [] {p : } (n : ) (hp : ) :
@[simp]
theorem Polynomial.coeff_pow_mul_natDegree {R : Type u} [] (p : ) (n : ) :
Polynomial.coeff (p ^ n) () =
theorem Polynomial.coeff_mul_add_eq_of_natDegree_le {R : Type u} [] {f : } {df : } {dg : } {g : } (hdf : ) (hdg : ) :
Polynomial.coeff (f * g) (df + dg) = *
theorem Polynomial.zero_le_degree_iff {R : Type u} [] {p : } :
p 0
theorem Polynomial.degree_le_iff_coeff_zero {R : Type u} [] (f : ) (n : ) :
∀ (m : ), n < m = 0
theorem Polynomial.degree_lt_iff_coeff_zero {R : Type u} [] (f : ) (n : ) :
∀ (m : ), n m = 0
theorem Polynomial.degree_smul_le {R : Type u} [] (a : R) (p : ) :
theorem Polynomial.natDegree_smul_le {R : Type u} [] (a : R) (p : ) :
theorem Polynomial.degree_lt_degree_mul_X {R : Type u} [] {p : } (hp : p 0) :
< Polynomial.degree (p * Polynomial.X)
theorem Polynomial.eq_C_of_natDegree_le_zero {R : Type u} [] {p : } (h : ) :
p = Polynomial.C ()
theorem Polynomial.eq_C_of_natDegree_eq_zero {R : Type u} [] {p : } (h : ) :
p = Polynomial.C ()
theorem Polynomial.natDegree_eq_zero {R : Type u} [] {p : } :
∃ (x : R), Polynomial.C x = p
theorem Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero {R : Type u} [] {p : } :
p = Polynomial.C ()
theorem Polynomial.eq_one_of_monic_natDegree_zero {R : Type u} [] {p : } (hf : ) (hfd : ) :
p = 1
theorem Polynomial.ne_zero_of_coe_le_degree {R : Type u} {n : } [] {p : } (hdeg : ) :
p 0
theorem Polynomial.le_natDegree_of_coe_le_degree {R : Type u} {n : } [] {p : } (hdeg : ) :
theorem Polynomial.degree_sum_fin_lt {R : Type u} [] {n : } (f : Fin nR) :
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} [] :
Polynomial.degree (Polynomial.C a * Polynomial.X + Polynomial.C b) 1
theorem Polynomial.degree_linear_lt {R : Type u} {a : R} {b : 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} [] (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} [] (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} [] :
Polynomial.natDegree (Polynomial.C a * Polynomial.X + Polynomial.C b) 1
theorem Polynomial.natDegree_linear {R : Type u} {a : R} {b : 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} [] (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} [] :
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} [] :
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} [] (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} [] (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} [] :
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} [] (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} [] (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} [] :
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} [] :
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} [] (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} [] (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} [] :
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} [] (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} [] (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} [] [] (n : ) :
Polynomial.degree (Polynomial.X ^ n) = n
@[simp]
theorem Polynomial.natDegree_X_pow {R : Type u} [] [] (n : ) :
Polynomial.natDegree (Polynomial.X ^ n) = n
@[simp]
theorem Polynomial.natDegree_mul_X {R : Type u} [] [] {p : } (hp : p 0) :
Polynomial.natDegree (p * Polynomial.X) =
@[simp]
theorem Polynomial.natDegree_X_mul {R : Type u} [] [] {p : } (hp : p 0) :
Polynomial.natDegree (Polynomial.X * p) =
@[simp]
theorem Polynomial.natDegree_mul_X_pow {R : Type u} [] [] {p : } (n : ) (hp : p 0) :
Polynomial.natDegree (p * Polynomial.X ^ n) =
@[simp]
theorem Polynomial.natDegree_X_pow_mul {R : Type u} [] [] {p : } (n : ) (hp : p 0) :
Polynomial.natDegree (Polynomial.X ^ n * p) =
theorem Polynomial.natDegree_X_pow_le {R : Type u_1} [] (n : ) :
Polynomial.natDegree (Polynomial.X ^ n) n
theorem Polynomial.not_isUnit_X {R : Type u} [] [] :
¬IsUnit Polynomial.X
@[simp]
theorem Polynomial.degree_mul_X {R : Type u} [] [] {p : } :
Polynomial.degree (p * Polynomial.X) =
@[simp]
theorem Polynomial.degree_mul_X_pow {R : Type u} [] [] {p : } (n : ) :
Polynomial.degree (p * Polynomial.X ^ n) =
theorem Polynomial.degree_sub_C {R : Type u} {a : R} [Ring R] {p : } (hp : ) :
Polynomial.degree (p - Polynomial.C a) =
@[simp]
theorem Polynomial.natDegree_sub_C {R : Type u} [Ring R] {p : } {a : R} :
Polynomial.natDegree (p - Polynomial.C a) =
theorem Polynomial.degree_sub_le {R : Type u} [Ring R] (p : ) (q : ) :
theorem Polynomial.degree_sub_le_of_le {R : Type u} [Ring R] {p : } {q : } {a : } {b : } (hp : ) (hq : ) :
theorem Polynomial.leadingCoeff_sub_of_degree_lt {R : Type u} [Ring R] {p : } {q : } (h : ) :
theorem Polynomial.leadingCoeff_sub_of_degree_lt' {R : Type u} [Ring R] {p : } {q : } (h : ) :
theorem Polynomial.leadingCoeff_sub_of_degree_eq {R : Type u} [Ring R] {p : } {q : } (h : ) (hlc : ) :
theorem Polynomial.natDegree_sub_le {R : Type u} [Ring R] (p : ) (q : ) :
theorem Polynomial.natDegree_sub_le_of_le {R : Type u} {n : } {m : } [Ring R] {p : } {q : } (hp : ) (hq : ) :
theorem Polynomial.degree_sub_lt {R : Type u} [Ring R] {p : } {q : } (hd : ) (hp0 : p 0) (hlc : ) :
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 : } {q : } (h : ) :
theorem Polynomial.degree_sub_eq_right_of_degree_lt {R : Type u} [Ring R] {p : } {q : } (h : ) :
theorem Polynomial.natDegree_sub_eq_left_of_natDegree_lt {R : Type u} [Ring R] {p : } {q : } (h : ) :
theorem Polynomial.natDegree_sub_eq_right_of_natDegree_lt {R : Type u} [Ring R] {p : } {q : } (h : ) :
@[simp]
theorem Polynomial.degree_X_add_C {R : Type u} [] [] (a : R) :
Polynomial.degree (Polynomial.X + Polynomial.C a) = 1
theorem Polynomial.natDegree_X_add_C {R : Type u} [] [] (x : R) :
Polynomial.natDegree (Polynomial.X + Polynomial.C x) = 1
@[simp]
theorem Polynomial.nextCoeff_X_add_C {S : Type v} [] (c : S) :
Polynomial.nextCoeff (Polynomial.X + Polynomial.C c) = c
theorem Polynomial.degree_X_pow_add_C {R : Type u} [] [] {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} [] [] {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.natDegree (Polynomial.X ^ n + Polynomial.C r) = 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.leadingCoeff (Polynomial.X ^ n + Polynomial.C r) = 1
@[simp]
Polynomial.leadingCoeff (Polynomial.X + Polynomial.C r) = 1
@[simp]
theorem Polynomial.leadingCoeff_X_pow_add_one {R : Type u} [] {n : } (hn : 0 < n) :
Polynomial.leadingCoeff (Polynomial.X ^ n + 1) = 1
@[simp]
theorem Polynomial.leadingCoeff_pow_X_add_C {R : Type u} [] (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] [] (a : R) :
Polynomial.degree (Polynomial.X - Polynomial.C a) = 1
theorem Polynomial.natDegree_X_sub_C {R : Type u} [Ring 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] [] {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] [] {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.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} [] [] {p : } {q : } :
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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Polynomial.degree_pow {R : Type u} [] [] [] (p : ) (n : ) :
@[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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Polynomial.leadingCoeffHom_apply {R : Type u} [] [] (p : ) :