mathlib documentation

data.polynomial.degree.definitions

Theory of univariate polynomials #

The definitions include degree, monic, leading_coeff

Results include

source
def polynomial.degree {R : Type u} [semiring R] (p : R[X]) :
with_bot ℕ

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

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

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

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

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

a polynomial is monic if its leading coefficient is 1

Equations
source
theorem polynomial.monic_of_subsingleton {R : Type u} [semiring R] [subsingleton R] (p : R[X]) :
p.monic
source
theorem polynomial.monic.def {R : Type u} [semiring R] {p : R[X]} :
p.monic ↔ p.leading_coeff = 1
source
@[protected, instance]
def polynomial.monic.decidable {R : Type u} [semiring R] {p : R[X]} [decidable_eq R] :
decidable p.monic
Equations
source
@[simp]
theorem polynomial.monic.leading_coeff {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) :
p.leading_coeff = 1
source
theorem polynomial.monic.coeff_nat_degree {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) :
p.coeff p.nat_degree = 1
source
@[simp]
theorem polynomial.degree_zero {R : Type u} [semiring R] :
0.degree = ⊥
source
@[simp]
theorem polynomial.nat_degree_zero {R : Type u} [semiring R] :
0.nat_degree = 0
source
@[simp]
theorem polynomial.coeff_nat_degree {R : Type u} [semiring R] {p : R[X]} :
p.coeff p.nat_degree = p.leading_coeff
source
theorem polynomial.degree_eq_bot {R : Type u} [semiring R] {p : R[X]} :
p.degree = ⊥ ↔ p = 0
source
theorem polynomial.degree_of_subsingleton {R : Type u} [semiring R] {p : R[X]} [subsingleton R] :
p.degree = ⊥
source
theorem polynomial.nat_degree_of_subsingleton {R : Type u} [semiring R] {p : R[X]} [subsingleton R] :
p.nat_degree = 0
source
theorem polynomial.degree_eq_nat_degree {R : Type u} [semiring R] {p : R[X]} (hp : p ≠ 0) :
p.degree = ↑(p.nat_degree)
source
theorem polynomial.degree_eq_iff_nat_degree_eq {R : Type u} [semiring R] {p : R[X]} {n : ℕ} (hp : p ≠ 0) :
p.degree = ↑n ↔ p.nat_degree = n
source
theorem polynomial.degree_eq_iff_nat_degree_eq_of_pos {R : Type u} [semiring R] {p : R[X]} {n : ℕ} (hn : 0 < n) :
p.degree = ↑n ↔ p.nat_degree = n
source
theorem polynomial.nat_degree_eq_of_degree_eq_some {R : Type u} [semiring R] {p : R[X]} {n : ℕ} (h : p.degree = ↑n) :
p.nat_degree = n
source
@[simp]
theorem polynomial.degree_le_nat_degree {R : Type u} [semiring R] {p : R[X]} :
p.degree ≤ ↑(p.nat_degree)
source
theorem polynomial.nat_degree_eq_of_degree_eq {R : Type u} {S : Type v} [semiring R] {p : R[X]} [semiring S] {q : S[X]} (h : p.degree = q.degree) :
p.nat_degree = q.nat_degree
source
theorem polynomial.le_degree_of_ne_zero {R : Type u} {n : ℕ} [semiring R] {p : R[X]} (h : p.coeff n ≠ 0) :
↑n ≤ p.degree
source
theorem polynomial.le_nat_degree_of_ne_zero {R : Type u} {n : ℕ} [semiring R] {p : R[X]} (h : p.coeff n ≠ 0) :
n ≤ p.nat_degree
source
theorem polynomial.le_nat_degree_of_mem_supp {R : Type u} [semiring R] {p : R[X]} (a : ℕ) :
a ∈ p.support → a ≤ p.nat_degree
source
theorem polynomial.degree_mono {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R[X]} {g : S[X]} (h : f.support ⊆ g.support) :
f.degree ≤ g.degree
source
theorem polynomial.supp_subset_range {R : Type u} {m : ℕ} [semiring R] {p : R[X]} (h : p.nat_degree < m) :
p.support ⊆ finset.range m
source
theorem polynomial.supp_subset_range_nat_degree_succ {R : Type u} [semiring R] {p : R[X]} :
p.support ⊆ finset.range (p.nat_degree + 1)
source
theorem polynomial.degree_le_degree {R : Type u} [semiring R] {p q : R[X]} (h : q.coeff p.nat_degree ≠ 0) :
p.degree ≤ q.degree
source
theorem polynomial.degree_ne_of_nat_degree_ne {R : Type u} [semiring R] {p : R[X]} {n : ℕ} :
p.nat_degree ≠ n → p.degree ≠ ↑n
source
theorem polynomial.nat_degree_le_iff_degree_le {R : Type u} [semiring R] {p : R[X]} {n : ℕ} :
p.nat_degree ≤ n ↔ p.degree ≤ ↑n
source
theorem polynomial.degree_le_of_nat_degree_le {R : Type u} [semiring R] {p : R[X]} {n : ℕ} :
p.nat_degree ≤ n → p.degree ≤ ↑n

Alias of polynomial.nat_degree_le_iff_degree_le.

source
theorem polynomial.nat_degree_le_of_degree_le {R : Type u} [semiring R] {p : R[X]} {n : ℕ} :
p.degree ≤ ↑n → p.nat_degree ≤ n

Alias of polynomial.nat_degree_le_iff_degree_le.

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

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

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

source
theorem polynomial.sum_fin {R : Type u} {S : Type v} [semiring R] [add_comm_monoid S] (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) {n : ℕ} {p : R[X]} (hn : p.degree < ↑n) :
∑ (i : fin n), f ↑i (p.coeff ↑i) = p.sum f
source
theorem polynomial.as_sum_range' {R : Type u} [semiring R] (p : R[X]) (n : ℕ) (w : p.nat_degree < n) :
p = ∑ (i : ℕ) in finset.range n, ⇑(polynomial.monomial i) (p.coeff i)
source
theorem polynomial.as_sum_range {R : Type u} [semiring R] (p : R[X]) :
p = ∑ (i : ℕ) in finset.range (p.nat_degree + 1), ⇑(polynomial.monomial i) (p.coeff i)
source
theorem polynomial.as_sum_range_C_mul_X_pow {R : Type u} [semiring R] (p : R[X]) :
p = ∑ (i : ℕ) in finset.range (p.nat_degree + 1), (⇑polynomial.C (p.coeff i)) * polynomial.X ^ i
source
theorem polynomial.coeff_ne_zero_of_eq_degree {R : Type u} {n : ℕ} [semiring R] {p : R[X]} (hn : p.degree = ↑n) :
p.coeff n ≠ 0
source
theorem polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [semiring R] {p : R[X]} (h : p.degree ≤ 1) :
p = (⇑polynomial.C (p.coeff 1)) * polynomial.X + ⇑polynomial.C (p.coeff 0)
source
theorem polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [semiring R] {p : R[X]} (h : p.degree = 1) :
p = (⇑polynomial.C p.leading_coeff) * polynomial.X + ⇑polynomial.C (p.coeff 0)
source
theorem polynomial.eq_X_add_C_of_nat_degree_le_one {R : Type u} [semiring R] {p : R[X]} (h : p.nat_degree ≤ 1) :
p = (⇑polynomial.C (p.coeff 1)) * polynomial.X + ⇑polynomial.C (p.coeff 0)
source
theorem polynomial.exists_eq_X_add_C_of_nat_degree_le_one {R : Type u} [semiring R] {p : R[X]} (h : p.nat_degree ≤ 1) :
∃ (a b : R), p = (⇑polynomial.C a) * polynomial.X + ⇑polynomial.C b
source
theorem polynomial.degree_X_pow_le {R : Type u} [semiring R] (n : ℕ) :
(polynomial.X ^ n).degree ≤ ↑n
source
theorem polynomial.degree_X_le {R : Type u} [semiring R] :
polynomial.X.degree ≤ 1
source
theorem polynomial.nat_degree_X_le {R : Type u} [semiring R] :
polynomial.X.nat_degree ≤ 1
source
theorem polynomial.support_C_mul_X_pow {R : Type u} [semiring R] (c : R) (n : ℕ) :
((⇑polynomial.C c) * polynomial.X ^ n).support ⊆ {n}
source
theorem polynomial.mem_support_C_mul_X_pow {R : Type u} [semiring R] {n a : ℕ} {c : R} (h : a ∈ ((⇑polynomial.C c) * polynomial.X ^ n).support) :
a = n
source
theorem polynomial.card_support_C_mul_X_pow_le_one {R : Type u} [semiring R] {c : R} {n : ℕ} :
((⇑polynomial.C c) * polynomial.X ^ n).support.card ≤ 1
source
theorem polynomial.card_supp_le_succ_nat_degree {R : Type u} [semiring R] (p : R[X]) :
p.support.card ≤ p.nat_degree + 1
source
theorem polynomial.le_degree_of_mem_supp {R : Type u} [semiring R] {p : R[X]} (a : ℕ) :
a ∈ p.support → ↑a ≤ p.degree
source
theorem polynomial.nonempty_support_iff {R : Type u} [semiring R] {p : R[X]} :
p.support.nonempty ↔ p ≠ 0
source
theorem polynomial.support_C_mul_X_pow_nonzero {R : Type u} [semiring R] {c : R} {n : ℕ} (h : c ≠ 0) :
((⇑polynomial.C c) * polynomial.X ^ n).support = {n}
source
@[simp]
theorem polynomial.degree_one {R : Type u} [semiring R] [nontrivial R] :
1.degree = 0
source
@[simp]
theorem polynomial.degree_X {R : Type u} [semiring R] [nontrivial R] :
polynomial.X.degree = 1
source
@[simp]
theorem polynomial.nat_degree_X {R : Type u} [semiring R] [nontrivial R] :
polynomial.X.nat_degree = 1
source
theorem polynomial.coeff_mul_X_sub_C {R : Type u} [ring R] {p : R[X]} {r : R} {a : ℕ} :
(p * (polynomial.X - ⇑polynomial.C r)).coeff (a + 1) = p.coeff a - (p.coeff (a + 1)) * r
source
@[simp]
theorem polynomial.degree_neg {R : Type u} [ring R] (p : R[X]) :
(-p).degree = p.degree
source
@[simp]
theorem polynomial.nat_degree_neg {R : Type u} [ring R] (p : R[X]) :
(-p).nat_degree = p.nat_degree
source
@[simp]
theorem polynomial.nat_degree_int_cast {R : Type u} [ring R] (n : ℤ) :
↑n.nat_degree = 0
source
def polynomial.next_coeff {R : Type u} [semiring R] (p : R[X]) :
R

The second-highest coefficient, or 0 for constants

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

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

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

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

Equations
source
@[simp]
theorem polynomial.leading_coeff_hom_apply {R : Type u} [semiring R] [no_zero_divisors R] (p : R[X]) :
⇑polynomial.leading_coeff_hom p = p.leading_coeff
source
@[simp]
theorem polynomial.leading_coeff_pow {R : Type u} [semiring R] [no_zero_divisors R] (p : R[X]) (n : ℕ) :
(p ^ n).leading_coeff = p.leading_coeff ^ n