# mathlibdocumentation

data.polynomial.degree.definitions

# Theory of univariate polynomials #

The definitions include `degree`, `monic`, `leading_coeff`

Results include

• `degree_mul` : The degree of the product is the sum of degrees
• `leading_coeff_add_of_degree_eq` and `leading_coeff_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) :

`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
theorem polynomial.degree_lt_wf {R : Type u} [semiring R] :
well_founded (λ (p q : , p.degree < q.degree)
@[protected, instance]
def polynomial.has_well_founded {R : Type u} [semiring R] :
Equations
def polynomial.nat_degree {R : Type u} [semiring R] (p : polynomial R) :

`nat_degree p` forces `degree p` to ℕ, by defining nat_degree 0 = 0.

Equations
def polynomial.leading_coeff {R : Type u} [semiring R] (p : polynomial R) :
R

`leading_coeff p` gives the coefficient of the highest power of `X` in `p`

Equations
def polynomial.monic {R : Type u} [semiring R] (p : polynomial R) :
Prop

a polynomial is `monic` if its leading coefficient is 1

Equations
Instances for `polynomial.monic`
theorem polynomial.monic_of_subsingleton {R : Type u} [semiring R] [subsingleton R] (p : polynomial R) :
theorem polynomial.monic.def {R : Type u} [semiring R] {p : polynomial R} :
@[protected, instance]
def polynomial.monic.decidable {R : Type u} [semiring R] {p : polynomial R} [decidable_eq R] :
Equations
@[simp]
theorem polynomial.monic.leading_coeff {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) :
theorem polynomial.monic.coeff_nat_degree {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) :
@[simp]
theorem polynomial.degree_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.nat_degree_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.coeff_nat_degree {R : Type u} [semiring R] {p : polynomial R} :
theorem polynomial.degree_eq_bot {R : Type u} [semiring R] {p : polynomial R} :
p.degree = p = 0
theorem polynomial.degree_eq_nat_degree {R : Type u} [semiring R] {p : polynomial R} (hp : p 0) :
theorem polynomial.degree_eq_iff_nat_degree_eq {R : Type u} [semiring R] {p : polynomial R} {n : } (hp : p 0) :
theorem polynomial.degree_eq_iff_nat_degree_eq_of_pos {R : Type u} [semiring R] {p : polynomial R} {n : } (hn : 0 < n) :
theorem polynomial.nat_degree_eq_of_degree_eq_some {R : Type u} [semiring R] {p : polynomial R} {n : } (h : p.degree = n) :
@[simp]
theorem polynomial.degree_le_nat_degree {R : Type u} [semiring R] {p : polynomial R} :
theorem polynomial.nat_degree_eq_of_degree_eq {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] {q : polynomial S} (h : p.degree = q.degree) :
theorem polynomial.le_degree_of_ne_zero {R : Type u} {n : } [semiring R] {p : polynomial R} (h : p.coeff n 0) :
theorem polynomial.le_nat_degree_of_ne_zero {R : Type u} {n : } [semiring R] {p : polynomial R} (h : p.coeff n 0) :
theorem polynomial.le_nat_degree_of_mem_supp {R : Type u} [semiring R] {p : polynomial R} (a : ) :
theorem polynomial.degree_mono {R : Type u} {S : Type v} [semiring R] [semiring S] {f : polynomial R} {g : polynomial S} (h : f.support g.support) :
theorem polynomial.supp_subset_range {R : Type u} {m : } [semiring R] {p : polynomial R} (h : p.nat_degree < m) :
theorem polynomial.degree_le_degree {R : Type u} [semiring R] {p q : polynomial R} (h : q.coeff p.nat_degree 0) :
theorem polynomial.degree_ne_of_nat_degree_ne {R : Type u} [semiring R] {p : polynomial R} {n : } :
theorem polynomial.nat_degree_lt_iff_degree_lt {R : Type u} {n : } [semiring R] {p : polynomial R} (hp : p 0) :
theorem polynomial.degree_le_of_nat_degree_le {R : Type u} [semiring R] {p : polynomial R} {n : } :

Alias of the forward direction of `polynomial.nat_degree_le_iff_degree_le`.

theorem polynomial.nat_degree_le_of_degree_le {R : Type u} [semiring R] {p : polynomial R} {n : } :

Alias of the reverse direction of `polynomial.nat_degree_le_iff_degree_le`.

theorem polynomial.nat_degree_le_nat_degree {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] {q : polynomial S} (hpq : p.degree q.degree) :
@[simp]
theorem polynomial.degree_C {R : Type u} {a : R} [semiring R] (ha : a 0) :
theorem polynomial.degree_C_le {R : Type u} {a : R} [semiring R] :
theorem polynomial.degree_C_lt {R : Type u} {a : R} [semiring R] :
theorem polynomial.degree_one_le {R : Type u} [semiring R] :
@[simp]
theorem polynomial.nat_degree_C {R : Type u} [semiring R] (a : R) :
= 0
@[simp]
theorem polynomial.nat_degree_one {R : Type u} [semiring R] :
@[simp]
theorem polynomial.nat_degree_nat_cast {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.degree_monomial {R : Type u} {a : R} [semiring R] (n : ) (ha : a 0) :
@[simp]
theorem polynomial.degree_C_mul_X_pow {R : Type u} {a : R} [semiring R] (n : ) (ha : a 0) :
theorem polynomial.degree_C_mul_X {R : Type u} {a : R} [semiring R] (ha : a 0) :
theorem polynomial.degree_monomial_le {R : Type u} [semiring R] (n : ) (a : R) :
theorem polynomial.degree_C_mul_X_pow_le {R : Type u} [semiring R] (n : ) (a : R) :
theorem polynomial.degree_C_mul_X_le {R : Type u} [semiring R] (a : R) :
@[simp]
theorem polynomial.nat_degree_C_mul_X_pow {R : Type u} [semiring R] (n : ) (a : R) (ha : a 0) :
@[simp]
theorem polynomial.nat_degree_C_mul_X {R : Type u} [semiring R] (a : R) (ha : a 0) :
@[simp]
theorem polynomial.nat_degree_monomial {R : Type u} [semiring R] [decidable_eq R] (i : ) (r : R) :
( r).nat_degree = ite (r = 0) 0 i
theorem polynomial.nat_degree_monomial_le {R : Type u} [semiring R] (a : R) {m : } :
theorem polynomial.nat_degree_monomial_eq {R : Type u} [semiring R] (i : ) {r : R} (r0 : r 0) :
theorem polynomial.coeff_eq_zero_of_degree_lt {R : Type u} {n : } [semiring R] {p : polynomial R} (h : p.degree < n) :
p.coeff n = 0
theorem polynomial.coeff_eq_zero_of_nat_degree_lt {R : Type u} [semiring R] {p : polynomial R} {n : } (h : p.nat_degree < n) :
p.coeff n = 0
@[simp]
theorem polynomial.coeff_nat_degree_succ_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p.coeff (p.nat_degree + 1) = 0
theorem polynomial.ite_le_nat_degree_coeff {R : Type u} [semiring R] (p : polynomial R) (n : ) (I : decidable (n < 1 + p.nat_degree)) :
ite (n < 1 + p.nat_degree) (p.coeff n) 0 = p.coeff n
theorem polynomial.as_sum_support {R : Type u} [semiring R] (p : polynomial R) :
p = p.support.sum (λ (i : ), (p.coeff i))
theorem polynomial.as_sum_support_C_mul_X_pow {R : Type u} [semiring R] (p : polynomial R) :
p = p.support.sum (λ (i : ), polynomial.C (p.coeff i) *
theorem polynomial.sum_over_range' {R : Type u} {S : Type v} [semiring R] (p : polynomial R) {f : R → S} (h : ∀ (n : ), f n 0 = 0) (n : ) (w : p.nat_degree < n) :
p.sum f = (finset.range n).sum (λ (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.nat_degree < n`.

theorem polynomial.sum_over_range {R : Type u} {S : Type v} [semiring R] (p : polynomial R) {f : R → S} (h : ∀ (n : ), f n 0 = 0) :
p.sum f = (finset.range (p.nat_degree + 1)).sum (λ (a : ), f a (p.coeff a))

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

theorem polynomial.sum_fin {R : Type u} {S : Type v} [semiring R] (f : R → S) (hf : ∀ (i : ), f i 0 = 0) {n : } {p : polynomial R} (hn : p.degree < n) :
finset.univ.sum (λ (i : fin n), f i (p.coeff i)) = p.sum f
theorem polynomial.as_sum_range' {R : Type u} [semiring R] (p : polynomial R) (n : ) (w : p.nat_degree < n) :
p = (finset.range n).sum (λ (i : ), (p.coeff i))
theorem polynomial.as_sum_range {R : Type u} [semiring R] (p : polynomial R) :
p = (finset.range (p.nat_degree + 1)).sum (λ (i : ), (p.coeff i))
theorem polynomial.as_sum_range_C_mul_X_pow {R : Type u} [semiring R] (p : polynomial R) :
p = (finset.range (p.nat_degree + 1)).sum (λ (i : ), polynomial.C (p.coeff i) *
theorem polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : } [semiring R] {p : polynomial R} (hn : p.degree = n) :
p.coeff n 0
theorem polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [semiring R] {p : polynomial R} (h : p.degree 1) :
theorem polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [semiring R] {p : polynomial R} (h : p.degree = 1) :
p =
theorem polynomial.exists_eq_X_add_C_of_nat_degree_le_one {R : Type u} [semiring R] {p : polynomial R} (h : p.nat_degree 1) :
∃ (a b : R),
theorem polynomial.degree_X_pow_le {R : Type u} [semiring R] (n : ) :
theorem polynomial.degree_X_le {R : Type u} [semiring R] :
theorem polynomial.nat_degree_X_le {R : Type u} [semiring R] :
theorem polynomial.mem_support_C_mul_X_pow {R : Type u} [semiring R] {n a : } {c : R} (h : a * .support) :
a = n
theorem polynomial.card_support_C_mul_X_pow_le_one {R : Type u} [semiring R] {c : R} {n : } :
theorem polynomial.le_degree_of_mem_supp {R : Type u} [semiring R] {p : polynomial R} (a : ) :
a p.supporta p.degree
theorem polynomial.nonempty_support_iff {R : Type u} [semiring R] {p : polynomial R} :
@[simp]
theorem polynomial.degree_one {R : Type u} [semiring R] [nontrivial R] :
1.degree = 0
@[simp]
theorem polynomial.degree_X {R : Type u} [semiring R] [nontrivial R] :
@[simp]
theorem polynomial.nat_degree_X {R : Type u} [semiring R] [nontrivial R] :
theorem polynomial.coeff_mul_X_sub_C {R : Type u} [ring R] {p : polynomial R} {r : R} {a : } :
(p * .coeff (a + 1) = p.coeff a - p.coeff (a + 1) * r
@[simp]
theorem polynomial.degree_neg {R : Type u} [ring R] (p : polynomial R) :
@[simp]
theorem polynomial.nat_degree_neg {R : Type u} [ring R] (p : polynomial R) :
@[simp]
theorem polynomial.nat_degree_int_cast {R : Type u} [ring R] (n : ) :
def polynomial.next_coeff {R : Type u} [semiring R] (p : polynomial R) :
R

The second-highest coefficient, or 0 for constants

Equations
@[simp]
theorem polynomial.next_coeff_C_eq_zero {R : Type u} [semiring R] (c : R) :
= 0
theorem polynomial.next_coeff_of_pos_nat_degree {R : Type u} [semiring R] (p : polynomial R) (hp : 0 < p.nat_degree) :
theorem polynomial.ne_zero_of_degree_gt {R : Type u} [semiring R] {p : polynomial R} {n : with_bot } (h : n < p.degree) :
p 0
theorem polynomial.ne_zero_of_degree_ge_degree {R : Type u} [semiring R] {p q : polynomial R} (hpq : p.degree q.degree) (hp : p 0) :
q 0
theorem polynomial.ne_zero_of_nat_degree_gt {R : Type u} [semiring R] {p : polynomial R} {n : } (h : n < p.nat_degree) :
p 0
theorem polynomial.degree_lt_degree {R : Type u} [semiring R] {p q : polynomial R} (h : p.nat_degree < q.nat_degree) :
theorem polynomial.nat_degree_lt_nat_degree_iff {R : Type u} [semiring R] {p q : polynomial R} (hp : p 0) :
theorem polynomial.eq_C_of_degree_le_zero {R : Type u} [semiring R] {p : polynomial R} (h : p.degree 0) :
theorem polynomial.eq_C_of_degree_eq_zero {R : Type u} [semiring R] {p : polynomial R} (h : p.degree = 0) :
theorem polynomial.degree_le_zero_iff {R : Type u} [semiring R] {p : polynomial R} :
theorem polynomial.degree_add_le {R : Type u} [semiring R] (p q : polynomial R) :
(p + q).degree
theorem polynomial.degree_add_le_of_degree_le {R : Type u} [semiring R] {p q : polynomial R} {n : } (hp : p.degree n) (hq : q.degree n) :
(p + q).degree n
theorem polynomial.nat_degree_add_le {R : Type u} [semiring R] (p q : polynomial R) :
theorem polynomial.nat_degree_add_le_of_degree_le {R : Type u} [semiring R] {p q : polynomial R} {n : } (hp : p.nat_degree n) (hq : q.nat_degree n) :
(p + q).nat_degree n
@[simp]
theorem polynomial.leading_coeff_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.leading_coeff_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p = 0
theorem polynomial.leading_coeff_ne_zero {R : Type u} [semiring R] {p : polynomial R} :
p 0
theorem polynomial.nat_degree_mem_support_of_nonzero {R : Type u} [semiring R] {p : polynomial R} (H : p 0) :
theorem polynomial.nat_degree_eq_support_max' {R : Type u} [semiring R] {p : polynomial R} (h : p 0) :
theorem polynomial.nat_degree_C_mul_X_pow_le {R : Type u} [semiring R] (a : R) (n : ) :
theorem polynomial.degree_add_eq_left_of_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (h : q.degree < p.degree) :
(p + q).degree = p.degree
theorem polynomial.degree_add_eq_right_of_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (h : p.degree < q.degree) :
(p + q).degree = q.degree
theorem polynomial.degree_add_C {R : Type u} {a : R} [semiring R] {p : polynomial R} (hp : 0 < p.degree) :
theorem polynomial.degree_add_eq_of_leading_coeff_add_ne_zero {R : Type u} [semiring R] {p q : polynomial R} (h : 0) :
(p + q).degree =
theorem polynomial.degree_erase_le {R : Type u} [semiring R] (p : polynomial R) (n : ) :
theorem polynomial.degree_erase_lt {R : Type u} [semiring R] {p : polynomial R} (hp : p 0) :
theorem polynomial.degree_update_le {R : Type u} [semiring R] (p : polynomial R) (n : ) (a : R) :
(p.update n a).degree
theorem polynomial.degree_sum_le {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι → ) :
(s.sum (λ (i : ι), f i)).degree s.sup (λ (b : ι), (f b).degree)
theorem polynomial.degree_mul_le {R : Type u} [semiring R] (p q : polynomial R) :
theorem polynomial.degree_pow_le {R : Type u} [semiring R] (p : polynomial R) (n : ) :
(p ^ n).degree n p.degree
@[simp]
theorem polynomial.leading_coeff_monomial {R : Type u} [semiring R] (a : R) (n : ) :
theorem polynomial.leading_coeff_C_mul_X_pow {R : Type u} [semiring R] (a : R) (n : ) :
theorem polynomial.leading_coeff_C_mul_X {R : Type u} [semiring R] (a : R) :
@[simp]
theorem polynomial.leading_coeff_C {R : Type u} [semiring R] (a : R) :
@[simp]
theorem polynomial.leading_coeff_X_pow {R : Type u} [semiring R] (n : ) :
= 1
@[simp]
theorem polynomial.leading_coeff_X {R : Type u} [semiring R] :
@[simp]
theorem polynomial.monic_X_pow {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.monic_X {R : Type u} [semiring R] :
@[simp]
theorem polynomial.leading_coeff_one {R : Type u} [semiring R] :
@[simp]
theorem polynomial.monic_one {R : Type u} [semiring R] :
theorem polynomial.monic.ne_zero {R : Type u_1} [semiring R] [nontrivial R] {p : polynomial R} (hp : p.monic) :
p 0
theorem polynomial.monic.ne_zero_of_ne {R : Type u} [semiring R] (h : 0 1) {p : polynomial R} (hp : p.monic) :
p 0
theorem polynomial.monic.ne_zero_of_polynomial_ne {R : Type u} [semiring R] {p q r : polynomial R} (hp : p.monic) (hne : q r) :
p 0
theorem polynomial.leading_coeff_add_of_degree_eq {R : Type u} [semiring R] {p q : polynomial R} (h : p.degree = q.degree) (hlc : 0) :
@[simp]
theorem polynomial.coeff_mul_degree_add_degree {R : Type u} [semiring R] (p q : polynomial R) :
theorem polynomial.degree_mul' {R : Type u} [semiring R] {p q : polynomial R} (h : 0) :
(p * q).degree = p.degree + q.degree
theorem polynomial.monic.degree_mul {R : Type u} [semiring R] {p q : polynomial R} (hq : q.monic) :
(p * q).degree = p.degree + q.degree
theorem polynomial.nat_degree_mul' {R : Type u} [semiring R] {p q : polynomial R} (h : 0) :
(p * q).nat_degree =
theorem polynomial.leading_coeff_mul' {R : Type u} [semiring R] {p q : polynomial R} (h : 0) :
theorem polynomial.C_mul_X_pow_eq_self {R : Type u} [semiring R] {p : polynomial R} (h : p.support.card 1) :
theorem polynomial.leading_coeff_pow' {R : Type u} {n : } [semiring R] {p : polynomial R} :
theorem polynomial.degree_pow' {R : Type u} [semiring R] {p : polynomial R} {n : } :
0(p ^ n).degree = n p.degree
theorem polynomial.nat_degree_pow' {R : Type u} [semiring R] {p : polynomial R} {n : } (h : 0) :
theorem polynomial.leading_coeff_monic_mul {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) :
theorem polynomial.leading_coeff_mul_monic {R : Type u} [semiring R] {p q : polynomial R} (hq : q.monic) :
@[simp]
theorem polynomial.leading_coeff_mul_X_pow {R : Type u} [semiring R] {p : polynomial R} {n : } :
@[simp]
theorem polynomial.leading_coeff_mul_X {R : Type u} [semiring R] {p : polynomial R} :
theorem polynomial.nat_degree_mul_le {R : Type u} [semiring R] {p q : polynomial R} :
theorem polynomial.nat_degree_pow_le {R : Type u} [semiring R] {p : polynomial R} {n : } :
@[simp]
theorem polynomial.coeff_pow_mul_nat_degree {R : Type u} [semiring R] (p : polynomial R) (n : ) :
(p ^ n).coeff (n * p.nat_degree) =
theorem polynomial.subsingleton_of_monic_zero {R : Type u} [semiring R] (h : 0.monic) :
(∀ (p q : , p = q) ∀ (a b : R), a = b
theorem polynomial.zero_le_degree_iff {R : Type u} [semiring R] {p : polynomial R} :
0 p.degree p 0
theorem polynomial.degree_nonneg_iff_ne_zero {R : Type u} [semiring R] {p : polynomial R} :
0 p.degree p 0
theorem polynomial.degree_le_iff_coeff_zero {R : Type u} [semiring R] (f : polynomial R) (n : with_bot ) :
f.degree n ∀ (m : ), n < mf.coeff m = 0
theorem polynomial.degree_lt_iff_coeff_zero {R : Type u} [semiring R] (f : polynomial R) (n : ) :
f.degree < n ∀ (m : ), n mf.coeff m = 0
theorem polynomial.degree_smul_le {R : Type u} [semiring R] (a : R) (p : polynomial R) :
theorem polynomial.nat_degree_smul_le {R : Type u} [semiring R] (a : R) (p : polynomial R) :
theorem polynomial.degree_lt_degree_mul_X {R : Type u} [semiring R] {p : polynomial R} (hp : p 0) :
theorem polynomial.eq_C_of_nat_degree_le_zero {R : Type u} [semiring R] {p : polynomial R} (h : p.nat_degree 0) :
theorem polynomial.eq_C_of_nat_degree_eq_zero {R : Type u} [semiring R] {p : polynomial R} (h : p.nat_degree = 0) :
theorem polynomial.ne_zero_of_coe_le_degree {R : Type u} {n : } [semiring R] {p : polynomial R} (hdeg : n p.degree) :
p 0
theorem polynomial.le_nat_degree_of_coe_le_degree {R : Type u} {n : } [semiring R] {p : polynomial R} (hdeg : n p.degree) :
theorem polynomial.degree_sum_fin_lt {R : Type u} [semiring R] {n : } (f : fin n → R) :
(finset.univ.sum (λ (i : fin n), polynomial.C (f i) * .degree < n
theorem polynomial.degree_linear_le {R : Type u} {a b : R} [semiring R] :
1
theorem polynomial.degree_linear_lt {R : Type u} {a b : R} [semiring R] :
< 2
theorem polynomial.degree_C_lt_degree_C_mul_X {R : Type u} {a b : R} [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.degree_linear {R : Type u} {a b : R} [semiring R] (ha : a 0) :
= 1
theorem polynomial.nat_degree_linear_le {R : Type u} {a b : R} [semiring R] :
@[simp]
theorem polynomial.nat_degree_linear {R : Type u} {a b : R} [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.leading_coeff_linear {R : Type u} {a b : R} [semiring R] (ha : a 0) :
theorem polynomial.degree_quadratic_le {R : Type u} {a b c : R} [semiring R] :
theorem polynomial.degree_quadratic_lt {R : Type u} {a b c : R} [semiring R] :
+ .degree < 3
theorem polynomial.degree_linear_lt_degree_C_mul_X_sq {R : Type u} {a b c : R} [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.degree_quadratic {R : Type u} {a b c : R} [semiring R] (ha : a 0) :
+ .degree = 2
theorem polynomial.nat_degree_quadratic_le {R : Type u} {a b c : R} [semiring R] :
@[simp]
theorem polynomial.nat_degree_quadratic {R : Type u} {a b c : R} [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.leading_coeff_quadratic {R : Type u} {a b c : R} [semiring R] (ha : a 0) :
= a
theorem polynomial.degree_cubic_le {R : Type u} {a b c d : R} [semiring R] :
+ + + .degree 3
theorem polynomial.degree_cubic_lt {R : Type u} {a b c d : R} [semiring R] :
+ + + .degree < 4
theorem polynomial.degree_quadratic_lt_degree_C_mul_X_cb {R : Type u} {a b c d : R} [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.degree_cubic {R : Type u} {a b c d : R} [semiring R] (ha : a 0) :
+ + + .degree = 3
theorem polynomial.nat_degree_cubic_le {R : Type u} {a b c d : R} [semiring R] :
@[simp]
theorem polynomial.nat_degree_cubic {R : Type u} {a b c d : R} [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.leading_coeff_cubic {R : Type u} {a b c d : R} [semiring R] (ha : a 0) :
@[simp]
theorem polynomial.degree_X_pow {R : Type u} [semiring R] [nontrivial R] (n : ) :
@[simp]
theorem polynomial.nat_degree_X_pow {R : Type u} [semiring R] [nontrivial R] (n : ) :
theorem polynomial.nat_degree_X_pow_le {R : Type u_1} [semiring R] (n : ) :
theorem polynomial.not_is_unit_X {R : Type u} [semiring R] [nontrivial R] :
@[simp]
theorem polynomial.degree_mul_X {R : Type u} [semiring R] [nontrivial R] {p : polynomial R} :
@[simp]
theorem polynomial.degree_mul_X_pow {R : Type u} {n : } [semiring R] [nontrivial R] {p : polynomial R} :
(p * .degree = p.degree + n
theorem polynomial.degree_sub_le {R : Type u} [ring R] (p q : polynomial R) :
(p - q).degree
theorem polynomial.degree_sub_lt {R : Type u} [ring R] {p q : polynomial R} (hd : p.degree = q.degree) (hp0 : p 0) (hlc : p.leading_coeff = q.leading_coeff) :
(p - q).degree < p.degree
theorem polynomial.nat_degree_X_sub_C_le {R : Type u} [ring R] {r : R} :
theorem polynomial.degree_sub_eq_left_of_degree_lt {R : Type u} [ring R] {p q : polynomial R} (h : q.degree < p.degree) :
(p - q).degree = p.degree
theorem polynomial.degree_sub_eq_right_of_degree_lt {R : Type u} [ring R] {p q : polynomial R} (h : p.degree < q.degree) :
(p - q).degree = q.degree
@[simp]
theorem polynomial.degree_X_add_C {R : Type u} [nontrivial R] [semiring R] (a : R) :
@[simp]
theorem polynomial.nat_degree_X_add_C {R : Type u} [nontrivial R] [semiring R] (x : R) :
@[simp]
theorem polynomial.next_coeff_X_add_C {S : Type v} [semiring S] (c : S) :
theorem polynomial.degree_X_pow_add_C {R : Type u} [nontrivial R] [semiring R] {n : } (hn : 0 < n) (a : R) :
theorem polynomial.X_pow_add_C_ne_zero {R : Type u} [nontrivial R] [semiring R] {n : } (hn : 0 < n) (a : R) :
0
theorem polynomial.X_add_C_ne_zero {R : Type u} [nontrivial R] [semiring R] (r : R) :
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 (λ (a : α), polynomial.X + polynomial.C (f a)) m
theorem polynomial.nat_degree_X_pow_add_C {R : Type u} [nontrivial R] [semiring R] {n : } {r : R} :
@[simp]
theorem polynomial.leading_coeff_X_pow_add_C {R : Type u} [semiring R] {n : } (hn : 0 < n) {r : R} :
@[simp]
theorem polynomial.leading_coeff_X_add_C {S : Type v} [semiring S] (r : S) :
@[simp]
theorem polynomial.leading_coeff_X_pow_add_one {R : Type u} [semiring R] {n : } (hn : 0 < n) :
@[simp]
theorem polynomial.leading_coeff_pow_X_add_C {R : Type u} [semiring R] (r : R) (i : ) :
@[simp]
theorem polynomial.leading_coeff_X_pow_sub_C {R : Type u} [ring R] {n : } (hn : 0 < n) {r : R} :
@[simp]
theorem polynomial.leading_coeff_X_pow_sub_one {R : Type u} [ring R] {n : } (hn : 0 < n) :
@[simp]
theorem polynomial.degree_X_sub_C {R : Type u} [ring R] [nontrivial R] (a : R) :
@[simp]
theorem polynomial.nat_degree_X_sub_C {R : Type u} [ring R] [nontrivial R] (x : R) :
@[simp]
theorem polynomial.next_coeff_X_sub_C {S : Type v} [ring S] (c : S) :
theorem polynomial.degree_X_pow_sub_C {R : Type u} [ring R] [nontrivial R] {n : } (hn : 0 < n) (a : R) :
theorem polynomial.X_pow_sub_C_ne_zero {R : Type u} [ring R] [nontrivial R] {n : } (hn : 0 < n) (a : R) :
0
theorem polynomial.X_sub_C_ne_zero {R : Type u} [ring R] [nontrivial R] (r : R) :
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 (λ (a : α), polynomial.X - polynomial.C (f a)) m
theorem polynomial.nat_degree_X_pow_sub_C {R : Type u} [ring R] [nontrivial R] {n : } {r : R} :
@[simp]
theorem polynomial.leading_coeff_X_sub_C {S : Type v} [ring S] (r : S) :
@[simp]
theorem polynomial.degree_mul {R : Type u} [semiring R] {p q : polynomial R} :
(p * q).degree = p.degree + q.degree
def polynomial.degree_monoid_hom {R : Type u} [semiring R] [nontrivial R] :

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

Equations
@[simp]
theorem polynomial.degree_pow {R : Type u} [semiring R] [nontrivial R] (p : polynomial R) (n : ) :
(p ^ n).degree = n p.degree
@[simp]
theorem polynomial.leading_coeff_mul {R : Type u} [semiring R] (p q : polynomial R) :
def polynomial.leading_coeff_hom {R : Type u} [semiring R]  :
→* R

`polynomial.leading_coeff` bundled as a `monoid_hom` when `R` has `no_zero_divisors`, and thus `leading_coeff` is multiplicative

Equations
@[simp]
theorem polynomial.leading_coeff_hom_apply {R : Type u} [semiring R] (p : polynomial R) :
@[simp]
theorem polynomial.leading_coeff_pow {R : Type u} [semiring R] (p : polynomial R) (n : ) :