Theory of degrees of polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Some of the main results include
nat_degree_comp_le: The degree of the composition is at most the product of degrees
theorem
polynomial.nat_degree_comp_le
{R : Type u}
[semiring R]
{p q : polynomial R} :
(p.comp q).nat_degree ≤ p.nat_degree * q.nat_degree
theorem
polynomial.degree_pos_of_root
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R}
(hp : p ≠ 0)
(h : p.is_root a) :
theorem
polynomial.nat_degree_le_iff_coeff_eq_zero
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R} :
theorem
polynomial.nat_degree_add_le_iff_left
{R : Type u}
[semiring R]
{n : ℕ}
(p q : polynomial R)
(qn : q.nat_degree ≤ n) :
(p + q).nat_degree ≤ n ↔ p.nat_degree ≤ n
theorem
polynomial.nat_degree_add_le_iff_right
{R : Type u}
[semiring R]
{n : ℕ}
(p q : polynomial R)
(pn : p.nat_degree ≤ n) :
(p + q).nat_degree ≤ n ↔ q.nat_degree ≤ n
theorem
polynomial.nat_degree_C_mul_le
{R : Type u}
[semiring R]
(a : R)
(f : polynomial R) :
(⇑polynomial.C a * f).nat_degree ≤ f.nat_degree
theorem
polynomial.nat_degree_mul_C_le
{R : Type u}
[semiring R]
(f : polynomial R)
(a : R) :
(f * ⇑polynomial.C a).nat_degree ≤ f.nat_degree
theorem
polynomial.eq_nat_degree_of_le_mem_support
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R}
(pn : p.nat_degree ≤ n)
(ns : n ∈ p.support) :
p.nat_degree = n
theorem
polynomial.nat_degree_C_mul_eq_of_mul_eq_one
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R}
{ai : R}
(au : ai * a = 1) :
(⇑polynomial.C a * p).nat_degree = p.nat_degree
theorem
polynomial.nat_degree_mul_C_eq_of_mul_eq_one
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R}
{ai : R}
(au : a * ai = 1) :
(p * ⇑polynomial.C a).nat_degree = p.nat_degree
theorem
polynomial.nat_degree_mul_C_eq_of_mul_ne_zero
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R}
(h : p.leading_coeff * a ≠ 0) :
(p * ⇑polynomial.C a).nat_degree = p.nat_degree
Although not explicitly stated, the assumptions of lemma nat_degree_mul_C_eq_of_mul_ne_zero
force the polynomial p to be non-zero, via p.leading_coeff ≠ 0.
theorem
polynomial.nat_degree_C_mul_eq_of_mul_ne_zero
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R}
(h : a * p.leading_coeff ≠ 0) :
(⇑polynomial.C a * p).nat_degree = p.nat_degree
Although not explicitly stated, the assumptions of lemma nat_degree_C_mul_eq_of_mul_ne_zero
force the polynomial p to be non-zero, via p.leading_coeff ≠ 0.
theorem
polynomial.nat_degree_add_coeff_mul
{R : Type u}
[semiring R]
(f g : polynomial R) :
(f * g).coeff (f.nat_degree + g.nat_degree) = f.coeff f.nat_degree * g.coeff g.nat_degree
theorem
polynomial.nat_degree_lt_coeff_mul
{R : Type u}
{m n : ℕ}
[semiring R]
{p q : polynomial R}
(h : p.nat_degree + q.nat_degree < m + n) :
theorem
polynomial.coeff_mul_of_nat_degree_le
{R : Type u}
{m n : ℕ}
[semiring R]
{p q : polynomial R}
(pm : p.nat_degree ≤ m)
(qn : q.nat_degree ≤ n) :
theorem
polynomial.coeff_pow_of_nat_degree_le
{R : Type u}
{m n : ℕ}
[semiring R]
{p : polynomial R}
(pn : p.nat_degree ≤ n) :
theorem
polynomial.coeff_add_eq_left_of_lt
{R : Type u}
{n : ℕ}
[semiring R]
{p q : polynomial R}
(qn : q.nat_degree < n) :
theorem
polynomial.coeff_add_eq_right_of_lt
{R : Type u}
{n : ℕ}
[semiring R]
{p q : polynomial R}
(pn : p.nat_degree < n) :
theorem
polynomial.nat_degree_sum_eq_of_disjoint
{R : Type u}
{S : Type v}
[semiring R]
(f : S → polynomial R)
(s : finset S)
(h : {i : S | i ∈ s ∧ f i ≠ 0}.pairwise (ne on polynomial.nat_degree ∘ f)) :
(s.sum f).nat_degree = s.sup (λ (i : S), (f i).nat_degree)
theorem
polynomial.nat_degree_bit0
{R : Type u}
[semiring R]
(a : polynomial R) :
(bit0 a).nat_degree ≤ a.nat_degree
theorem
polynomial.nat_degree_bit1
{R : Type u}
[semiring R]
(a : polynomial R) :
(bit1 a).nat_degree ≤ a.nat_degree
theorem
polynomial.nat_degree_pos_of_eval₂_root
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{p : polynomial R}
(hp : p ≠ 0)
(f : R →+* S)
{z : S}
(hz : polynomial.eval₂ f z p = 0)
(inj : ∀ (x : R), ⇑f x = 0 → x = 0) :
0 < p.nat_degree
@[simp]
theorem
polynomial.nat_degree_sub
{R : Type u}
[ring R]
{p q : polynomial R} :
(p - q).nat_degree = (q - p).nat_degree
theorem
polynomial.nat_degree_sub_le_iff_left
{R : Type u}
{n : ℕ}
[ring R]
{p q : polynomial R}
(qn : q.nat_degree ≤ n) :
(p - q).nat_degree ≤ n ↔ p.nat_degree ≤ n
theorem
polynomial.nat_degree_sub_le_iff_right
{R : Type u}
{n : ℕ}
[ring R]
{p q : polynomial R}
(pn : p.nat_degree ≤ n) :
(p - q).nat_degree ≤ n ↔ q.nat_degree ≤ n
theorem
polynomial.coeff_sub_eq_left_of_lt
{R : Type u}
{n : ℕ}
[ring R]
{p q : polynomial R}
(dg : q.nat_degree < n) :
theorem
polynomial.coeff_sub_eq_neg_right_of_lt
{R : Type u}
{n : ℕ}
[ring R]
{p q : polynomial R}
(df : p.nat_degree < n) :
theorem
polynomial.degree_mul_C
{R : Type u}
{a : R}
[semiring R]
[no_zero_divisors R]
{p : polynomial R}
(a0 : a ≠ 0) :
theorem
polynomial.degree_C_mul
{R : Type u}
{a : R}
[semiring R]
[no_zero_divisors R]
{p : polynomial R}
(a0 : a ≠ 0) :
theorem
polynomial.nat_degree_mul_C
{R : Type u}
{a : R}
[semiring R]
[no_zero_divisors R]
{p : polynomial R}
(a0 : a ≠ 0) :
(p * ⇑polynomial.C a).nat_degree = p.nat_degree
theorem
polynomial.nat_degree_C_mul
{R : Type u}
{a : R}
[semiring R]
[no_zero_divisors R]
{p : polynomial R}
(a0 : a ≠ 0) :
(⇑polynomial.C a * p).nat_degree = p.nat_degree
theorem
polynomial.nat_degree_comp
{R : Type u}
[semiring R]
[no_zero_divisors R]
{p q : polynomial R} :
(p.comp q).nat_degree = p.nat_degree * q.nat_degree
@[simp]
theorem
polynomial.nat_degree_iterate_comp
{R : Type u}
[semiring R]
[no_zero_divisors R]
{p q : polynomial R}
(k : ℕ) :
(p.comp^[k] q).nat_degree = p.nat_degree ^ k * q.nat_degree
theorem
polynomial.leading_coeff_comp
{R : Type u}
[semiring R]
[no_zero_divisors R]
{p q : polynomial R}
(hq : q.nat_degree ≠ 0) :
(p.comp q).leading_coeff = p.leading_coeff * q.leading_coeff ^ p.nat_degree