Theory of univariate polynomials
The definitions include
degree, monic, leading_coeff
Results include
degree_mul: The degree of the product is the sum of degreesleading_coeff_add_of_degree_eqandleading_coeff_add_of_degree_lt: The leading_coefficient of a sum is determined by the leading coefficients and degrees
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.sup option.some
theorem
polynomial.degree_lt_wf
{R : Type u}
[semiring R] :
well_founded (λ (p q : polynomial R), p.degree < q.degree)
@[instance]
Equations
- polynomial.has_well_founded = {r := λ (p q : polynomial R), p.degree < q.degree, wf := _}
nat_degree p forces degree p to ℕ, by defining nat_degree 0 = 0.
Equations
- p.nat_degree = option.get_or_else p.degree 0
leading_coeff p gives the coefficient of the highest power of X in p
Equations
- p.leading_coeff = p.coeff p.nat_degree
a polynomial is monic if its leading coefficient is 1
Equations
- p.monic = (p.leading_coeff = 1)
theorem
polynomial.monic.def
{R : Type u}
[semiring R]
{p : polynomial R} :
p.monic ↔ p.leading_coeff = 1
@[instance]
Equations
- polynomial.monic.decidable = polynomial.monic.decidable._proof_1.mpr (_inst_2 p.leading_coeff 1)
@[simp]
theorem
polynomial.monic.leading_coeff
{R : Type u}
[semiring R]
{p : polynomial R} :
p.monic → p.leading_coeff = 1
theorem
polynomial.degree_eq_nat_degree
{R : Type u}
[semiring R]
{p : polynomial R} :
p ≠ 0 → p.degree = ↑(p.nat_degree)
theorem
polynomial.degree_eq_iff_nat_degree_eq
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
theorem
polynomial.degree_eq_iff_nat_degree_eq_of_pos
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
theorem
polynomial.nat_degree_eq_of_degree_eq_some
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
p.degree = ↑n → p.nat_degree = n
@[simp]
theorem
polynomial.degree_le_nat_degree
{R : Type u}
[semiring R]
{p : polynomial R} :
p.degree ≤ ↑(p.nat_degree)
theorem
polynomial.nat_degree_eq_of_degree_eq
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
{q : polynomial S} :
p.degree = q.degree → p.nat_degree = q.nat_degree
theorem
polynomial.le_nat_degree_of_ne_zero
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R} :
p.coeff n ≠ 0 → n ≤ p.nat_degree
theorem
polynomial.degree_ne_of_nat_degree_ne
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
p.nat_degree ≠ n → p.degree ≠ ↑n
theorem
polynomial.nat_degree_le_of_degree_le
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
p.degree ≤ ↑n → p.nat_degree ≤ n
theorem
polynomial.nat_degree_le_nat_degree
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.degree ≤ q.degree → p.nat_degree ≤ q.nat_degree
@[simp]
theorem
polynomial.degree_C
{R : Type u}
{a : R}
[semiring R] :
a ≠ 0 → (⇑polynomial.C a).degree = 0
@[simp]
theorem
polynomial.nat_degree_C
{R : Type u}
[semiring R]
(a : R) :
(⇑polynomial.C a).nat_degree = 0
@[simp]
@[simp]
theorem
polynomial.degree_monomial
{R : Type u}
{a : R}
[semiring R]
(n : ℕ) :
a ≠ 0 → (⇑polynomial.C a * polynomial.X ^ n).degree = ↑n
theorem
polynomial.degree_monomial_le
{R : Type u}
[semiring R]
(n : ℕ)
(a : R) :
(⇑polynomial.C a * polynomial.X ^ n).degree ≤ ↑n
theorem
polynomial.coeff_eq_zero_of_degree_lt
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R} :
theorem
polynomial.coeff_eq_zero_of_nat_degree_lt
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
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)) :
theorem
polynomial.as_sum
{R : Type u}
[semiring R]
(p : polynomial R) :
p = (finset.range (p.nat_degree + 1)).sum (λ (i : ℕ), ⇑polynomial.C (p.coeff i) * polynomial.X ^ i)
theorem
polynomial.sum_over_range'
{R : Type u}
{S : Type v}
[semiring R]
[add_comm_monoid S]
(p : polynomial R)
{f : ℕ → R → S}
(h : ∀ (n : ℕ), f n 0 = 0)
(n : ℕ) :
p.nat_degree < n → finsupp.sum p 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]
[add_comm_monoid S]
(p : polynomial R)
{f : ℕ → R → S} :
(∀ (n : ℕ), f n 0 = 0) → finsupp.sum p 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.coeff_ne_zero_of_eq_degree
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R} :
theorem
polynomial.eq_X_add_C_of_degree_le_one
{R : Type u}
[semiring R]
{p : polynomial R} :
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}
[semiring R]
{p : polynomial R} :
p.degree = 1 → p = ⇑polynomial.C p.leading_coeff * polynomial.X + ⇑polynomial.C (p.coeff 0)
theorem
polynomial.degree_C_mul_X_pow_le
{R : Type u}
[semiring R]
(r : R)
(n : ℕ) :
(⇑polynomial.C r * polynomial.X ^ n).degree ≤ ↑n
theorem
polynomial.degree_X_pow_le
{R : Type u}
[semiring R]
(n : ℕ) :
(polynomial.X ^ n).degree ≤ ↑n
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.nat_degree_neg
{R : Type u}
[ring R]
(p : polynomial R) :
(-p).nat_degree = p.nat_degree
@[simp]
The second-highest coefficient, or 0 for constants
Equations
- p.next_coeff = ite (p.nat_degree = 0) 0 (p.coeff (p.nat_degree - 1))
@[simp]
theorem
polynomial.next_coeff_C_eq_zero
{R : Type u}
[semiring R]
(c : R) :
(⇑polynomial.C c).next_coeff = 0
theorem
polynomial.next_coeff_of_pos_nat_degree
{R : Type u}
[semiring R]
(p : polynomial R) :
0 < p.nat_degree → p.next_coeff = p.coeff (p.nat_degree - 1)
theorem
polynomial.coeff_nat_degree_eq_zero_of_degree_lt
{R : Type u}
[semiring R]
{p q : polynomial R} :
theorem
polynomial.ne_zero_of_degree_gt
{R : Type u}
[semiring R]
{p : polynomial R}
{n : with_bot ℕ} :
@[simp]
@[simp]
theorem
polynomial.leading_coeff_eq_zero
{R : Type u}
[semiring R]
{p : polynomial R} :
p.leading_coeff = 0 ↔ p = 0
theorem
polynomial.leading_coeff_eq_zero_iff_deg_eq_bot
{R : Type u}
[semiring R]
{p : polynomial R} :
theorem
polynomial.degree_add_eq_of_leading_coeff_add_ne_zero
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.leading_coeff + q.leading_coeff ≠ 0 → (p + q).degree = max p.degree q.degree
theorem
polynomial.degree_erase_le
{R : Type u}
[semiring R]
(p : polynomial R)
(n : ℕ) :
polynomial.degree (finsupp.erase n p) ≤ p.degree
theorem
polynomial.degree_erase_lt
{R : Type u}
[semiring R]
{p : polynomial R} :
p ≠ 0 → polynomial.degree (finsupp.erase p.nat_degree p) < p.degree
theorem
polynomial.degree_sum_le
{R : Type u}
[semiring R]
{ι : Type u_1}
(s : finset ι)
(f : ι → polynomial R) :
@[simp]
theorem
polynomial.leading_coeff_monomial
{R : Type u}
[semiring R]
(a : R)
(n : ℕ) :
(⇑polynomial.C a * polynomial.X ^ n).leading_coeff = a
@[simp]
theorem
polynomial.leading_coeff_C
{R : Type u}
[semiring R]
(a : R) :
(⇑polynomial.C a).leading_coeff = a
@[simp]
@[simp]
theorem
polynomial.monic.ne_zero_of_zero_ne_one
{R : Type u}
[semiring R]
(h : 0 ≠ 1)
{p : polynomial R} :
theorem
polynomial.leading_coeff_add_of_degree_lt
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.degree < q.degree → (p + q).leading_coeff = q.leading_coeff
theorem
polynomial.leading_coeff_add_of_degree_eq
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.degree = q.degree → p.leading_coeff + q.leading_coeff ≠ 0 → (p + q).leading_coeff = p.leading_coeff + q.leading_coeff
@[simp]
theorem
polynomial.coeff_mul_degree_add_degree
{R : Type u}
[semiring R]
(p q : polynomial R) :
(p * q).coeff (p.nat_degree + q.nat_degree) = p.leading_coeff * q.leading_coeff
theorem
polynomial.degree_mul'
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.leading_coeff * q.leading_coeff ≠ 0 → (p * q).degree = p.degree + q.degree
theorem
polynomial.nat_degree_mul'
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.leading_coeff * q.leading_coeff ≠ 0 → (p * q).nat_degree = p.nat_degree + q.nat_degree
theorem
polynomial.leading_coeff_mul'
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.leading_coeff * q.leading_coeff ≠ 0 → (p * q).leading_coeff = p.leading_coeff * q.leading_coeff
theorem
polynomial.leading_coeff_pow'
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R} :
p.leading_coeff ^ n ≠ 0 → (p ^ n).leading_coeff = p.leading_coeff ^ n
theorem
polynomial.nat_degree_pow'
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
p.leading_coeff ^ n ≠ 0 → (p ^ n).nat_degree = n * p.nat_degree
@[simp]
theorem
polynomial.leading_coeff_X_pow
{R : Type u}
[semiring R]
(n : ℕ) :
(polynomial.X ^ n).leading_coeff = 1
theorem
polynomial.leading_coeff_mul_X_pow
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
(p * polynomial.X ^ n).leading_coeff = p.leading_coeff
theorem
polynomial.nat_degree_mul_le
{R : Type u}
[semiring R]
{p q : polynomial R} :
(p * q).nat_degree ≤ p.nat_degree + q.nat_degree
theorem
polynomial.subsingleton_of_monic_zero
{R : Type u}
[semiring R] :
0.monic → ((∀ (p q : polynomial R), p = q) ∧ ∀ (a b : R), a = b)
theorem
polynomial.nat_degree_eq_zero_iff_degree_le_zero
{R : Type u}
[semiring R]
{p : polynomial R} :
p.nat_degree = 0 ↔ p.degree ≤ 0
theorem
polynomial.eq_C_of_nat_degree_le_zero
{R : Type u}
[semiring R]
{p : polynomial R} :
p.nat_degree ≤ 0 → p = ⇑polynomial.C (p.coeff 0)
theorem
polynomial.nat_degree_pos_iff_degree_pos
{R : Type u}
[semiring R]
{p : polynomial R} :
0 < p.nat_degree ↔ 0 < p.degree
@[simp]
theorem
polynomial.degree_X_pow
{R : Type u}
[semiring R]
[nontrivial R]
(n : ℕ) :
(polynomial.X ^ n).degree = ↑n
theorem
polynomial.nat_degree_X_sub_C_le
{R : Type u}
[ring R]
{r : R} :
(polynomial.X - ⇑polynomial.C r).nat_degree ≤ 1
@[simp]
theorem
polynomial.degree_X_sub_C
{R : Type u}
[nontrivial R]
[ring R]
(a : R) :
(polynomial.X - ⇑polynomial.C a).degree = 1
@[simp]
theorem
polynomial.nat_degree_X_sub_C
{R : Type u}
[nontrivial R]
[ring R]
(x : R) :
(polynomial.X - ⇑polynomial.C x).nat_degree = 1
@[simp]
theorem
polynomial.next_coeff_X_sub_C
{R : Type u}
[nontrivial R]
[ring R]
(c : R) :
(polynomial.X - ⇑polynomial.C c).next_coeff = -c
theorem
polynomial.degree_X_pow_sub_C
{R : Type u}
[nontrivial R]
[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}
[nontrivial R]
[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}
[nontrivial R]
[ring R]
(r : R) :
polynomial.X - ⇑polynomial.C r ≠ 0
theorem
polynomial.nat_degree_X_pow_sub_C
{R : Type u}
[nontrivial R]
[ring R]
{n : ℕ}
(hn : 0 < n)
{r : R} :
(polynomial.X ^ n - ⇑polynomial.C r).nat_degree = n
@[simp]
@[simp]
@[simp]
theorem
polynomial.leading_coeff_mul
{R : Type u}
[integral_domain R]
(p q : polynomial R) :
(p * q).leading_coeff = p.leading_coeff * q.leading_coeff
@[simp]
theorem
polynomial.leading_coeff_X_add_C
{R : Type u}
[integral_domain R]
(a b : R) :
a ≠ 0 → (⇑polynomial.C a * polynomial.X + ⇑polynomial.C b).leading_coeff = a
polynomial.leading_coeff bundled as a monoid_hom when R is an integral_domain, and thus
leading_coeff is multiplicative
Equations
@[simp]
@[simp]
theorem
polynomial.leading_coeff_pow
{R : Type u}
[integral_domain R]
(p : polynomial R)
(n : ℕ) :
(p ^ n).leading_coeff = p.leading_coeff ^ n