Theory of degrees of polynomials #
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 : R[X]} :
(p.comp q).nat_degree ≤ (p.nat_degree) * q.nat_degree
theorem
polynomial.nat_degree_C_mul_le
{R : Type u}
[semiring R]
(a : R)
(f : R[X]) :
((⇑polynomial.C a) * f).nat_degree ≤ f.nat_degree
theorem
polynomial.nat_degree_mul_C_le
{R : Type u}
[semiring R]
(f : R[X])
(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 : R[X]}
(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 : R[X]}
{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 : R[X]}
{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 : R[X]}
(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 : R[X]}
(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 : R[X]) :
(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 : R[X]}
(h : p.nat_degree + q.nat_degree < m + n) :
theorem
polynomial.nat_degree_sum_eq_of_disjoint
{R : Type u}
{S : Type v}
[semiring R]
(f : S → R[X])
(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_pos_of_eval₂_root
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{p : R[X]}
(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
theorem
polynomial.degree_mul_C
{R : Type u}
{a : R}
[semiring R]
[no_zero_divisors R]
{p : R[X]}
(a0 : a ≠ 0) :
theorem
polynomial.degree_C_mul
{R : Type u}
{a : R}
[semiring R]
[no_zero_divisors R]
{p : R[X]}
(a0 : a ≠ 0) :
theorem
polynomial.nat_degree_mul_C
{R : Type u}
{a : R}
[semiring R]
[no_zero_divisors R]
{p : R[X]}
(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 : R[X]}
(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 : R[X]} :
(p.comp q).nat_degree = (p.nat_degree) * q.nat_degree
theorem
polynomial.leading_coeff_comp
{R : Type u}
[semiring R]
[no_zero_divisors R]
{p q : R[X]}
(hq : q.nat_degree ≠ 0) :
(p.comp q).leading_coeff = (p.leading_coeff) * q.leading_coeff ^ p.nat_degree