Theory of degrees of polynomials #
Some of the main results include
natDegree_comp_le: The degree of the composition is at most the product of degrees
theorem
Polynomial.natDegree_comp_le
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
:
theorem
Polynomial.degree_pos_of_root
{R : Type u}
{a : R}
[Semiring R]
{p : Polynomial R}
(hp : p ≠ 0)
(h : Polynomial.IsRoot p a)
:
0 < Polynomial.degree p
theorem
Polynomial.natDegree_le_iff_coeff_eq_zero
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
:
Polynomial.natDegree p ≤ n ↔ ∀ (N : ℕ), n < N → Polynomial.coeff p N = 0
theorem
Polynomial.natDegree_add_le_iff_left
{R : Type u}
[Semiring R]
{n : ℕ}
(p : Polynomial R)
(q : Polynomial R)
(qn : Polynomial.natDegree q ≤ n)
:
Polynomial.natDegree (p + q) ≤ n ↔ Polynomial.natDegree p ≤ n
theorem
Polynomial.natDegree_add_le_iff_right
{R : Type u}
[Semiring R]
{n : ℕ}
(p : Polynomial R)
(q : Polynomial R)
(pn : Polynomial.natDegree p ≤ n)
:
Polynomial.natDegree (p + q) ≤ n ↔ Polynomial.natDegree q ≤ n
theorem
Polynomial.natDegree_C_mul_le
{R : Type u}
[Semiring R]
(a : R)
(f : Polynomial R)
:
Polynomial.natDegree (Polynomial.C a * f) ≤ Polynomial.natDegree f
theorem
Polynomial.natDegree_mul_C_le
{R : Type u}
[Semiring R]
(f : Polynomial R)
(a : R)
:
Polynomial.natDegree (f * Polynomial.C a) ≤ Polynomial.natDegree f
theorem
Polynomial.eq_natDegree_of_le_mem_support
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
(pn : Polynomial.natDegree p ≤ n)
(ns : n ∈ Polynomial.support p)
:
theorem
Polynomial.natDegree_C_mul_eq_of_mul_eq_one
{R : Type u}
{a : R}
[Semiring R]
{p : Polynomial R}
{ai : R}
(au : ai * a = 1)
:
Polynomial.natDegree (Polynomial.C a * p) = Polynomial.natDegree p
theorem
Polynomial.natDegree_mul_C_eq_of_mul_eq_one
{R : Type u}
{a : R}
[Semiring R]
{p : Polynomial R}
{ai : R}
(au : a * ai = 1)
:
Polynomial.natDegree (p * Polynomial.C a) = Polynomial.natDegree p
theorem
Polynomial.natDegree_mul_C_eq_of_mul_ne_zero
{R : Type u}
{a : R}
[Semiring R]
{p : Polynomial R}
(h : Polynomial.leadingCoeff p * a ≠ 0)
:
Polynomial.natDegree (p * Polynomial.C a) = Polynomial.natDegree p
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.natDegree_C_mul_eq_of_mul_ne_zero
{R : Type u}
{a : R}
[Semiring R]
{p : Polynomial R}
(h : a * Polynomial.leadingCoeff p ≠ 0)
:
Polynomial.natDegree (Polynomial.C a * p) = Polynomial.natDegree p
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.natDegree_add_coeff_mul
{R : Type u}
[Semiring R]
(f : Polynomial R)
(g : Polynomial R)
:
Polynomial.coeff (f * g) (Polynomial.natDegree f + Polynomial.natDegree g) = Polynomial.coeff f (Polynomial.natDegree f) * Polynomial.coeff g (Polynomial.natDegree g)
theorem
Polynomial.natDegree_lt_coeff_mul
{R : Type u}
{m : ℕ}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(h : Polynomial.natDegree p + Polynomial.natDegree q < m + n)
:
Polynomial.coeff (p * q) (m + n) = 0
theorem
Polynomial.coeff_mul_of_natDegree_le
{R : Type u}
{m : ℕ}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(pm : Polynomial.natDegree p ≤ m)
(qn : Polynomial.natDegree q ≤ n)
:
Polynomial.coeff (p * q) (m + n) = Polynomial.coeff p m * Polynomial.coeff q n
theorem
Polynomial.coeff_pow_of_natDegree_le
{R : Type u}
{m : ℕ}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
(pn : Polynomial.natDegree p ≤ n)
:
Polynomial.coeff (p ^ m) (m * n) = Polynomial.coeff p n ^ m
theorem
Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le
{R : Type u}
{m : ℕ}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{o : ℕ}
(pn : Polynomial.natDegree p ≤ n)
(mno : m * n ≤ o)
:
Polynomial.coeff (p ^ m) o = if o = m * n then Polynomial.coeff p n ^ m else 0
theorem
Polynomial.coeff_add_eq_left_of_lt
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(qn : Polynomial.natDegree q < n)
:
Polynomial.coeff (p + q) n = Polynomial.coeff p n
theorem
Polynomial.coeff_add_eq_right_of_lt
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(pn : Polynomial.natDegree p < n)
:
Polynomial.coeff (p + q) n = Polynomial.coeff q n
theorem
Polynomial.degree_sum_eq_of_disjoint
{R : Type u}
{S : Type v}
[Semiring R]
(f : S → Polynomial R)
(s : Finset S)
(h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on Polynomial.degree ∘ f))
:
Polynomial.degree (Finset.sum s f) = Finset.sup s fun (i : S) => Polynomial.degree (f i)
theorem
Polynomial.natDegree_sum_eq_of_disjoint
{R : Type u}
{S : Type v}
[Semiring R]
(f : S → Polynomial R)
(s : Finset S)
(h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on Polynomial.natDegree ∘ f))
:
Polynomial.natDegree (Finset.sum s f) = Finset.sup s fun (i : S) => Polynomial.natDegree (f i)
theorem
Polynomial.natDegree_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)
:
theorem
Polynomial.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 < Polynomial.degree p
@[simp]
theorem
Polynomial.coe_lt_degree
{R : Type u}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
:
↑n < Polynomial.degree p ↔ n < Polynomial.natDegree p
@[simp]
theorem
Polynomial.degree_map_eq_iff
{R : Type u}
{S : Type v}
[Semiring R]
[Semiring S]
{f : R →+* S}
{p : Polynomial R}
:
Polynomial.degree (Polynomial.map f p) = Polynomial.degree p ↔ f (Polynomial.leadingCoeff p) ≠ 0 ∨ p = 0
@[simp]
theorem
Polynomial.natDegree_map_eq_iff
{R : Type u}
{S : Type v}
[Semiring R]
[Semiring S]
{f : R →+* S}
{p : Polynomial R}
:
Polynomial.natDegree (Polynomial.map f p) = Polynomial.natDegree p ↔ f (Polynomial.leadingCoeff p) ≠ 0 ∨ Polynomial.natDegree p = 0
theorem
Polynomial.natDegree_pos_of_nextCoeff_ne_zero
{R : Type u}
[Semiring R]
{p : Polynomial R}
(h : Polynomial.nextCoeff p ≠ 0)
:
theorem
Polynomial.natDegree_sub
{R : Type u}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
:
Polynomial.natDegree (p - q) = Polynomial.natDegree (q - p)
theorem
Polynomial.natDegree_sub_le_iff_left
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(qn : Polynomial.natDegree q ≤ n)
:
Polynomial.natDegree (p - q) ≤ n ↔ Polynomial.natDegree p ≤ n
theorem
Polynomial.natDegree_sub_le_iff_right
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(pn : Polynomial.natDegree p ≤ n)
:
Polynomial.natDegree (p - q) ≤ n ↔ Polynomial.natDegree q ≤ n
theorem
Polynomial.coeff_sub_eq_left_of_lt
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(dg : Polynomial.natDegree q < n)
:
Polynomial.coeff (p - q) n = Polynomial.coeff p n
theorem
Polynomial.coeff_sub_eq_neg_right_of_lt
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(df : Polynomial.natDegree p < n)
:
Polynomial.coeff (p - q) n = -Polynomial.coeff q n
theorem
Polynomial.degree_mul_C
{R : Type u}
[Semiring R]
[NoZeroDivisors R]
{p : Polynomial R}
{a : R}
(a0 : a ≠ 0)
:
Polynomial.degree (p * Polynomial.C a) = Polynomial.degree p
theorem
Polynomial.degree_C_mul
{R : Type u}
[Semiring R]
[NoZeroDivisors R]
{p : Polynomial R}
{a : R}
(a0 : a ≠ 0)
:
Polynomial.degree (Polynomial.C a * p) = Polynomial.degree p
theorem
Polynomial.natDegree_mul_C
{R : Type u}
[Semiring R]
[NoZeroDivisors R]
{p : Polynomial R}
{a : R}
(a0 : a ≠ 0)
:
Polynomial.natDegree (p * Polynomial.C a) = Polynomial.natDegree p
theorem
Polynomial.natDegree_C_mul
{R : Type u}
[Semiring R]
[NoZeroDivisors R]
{p : Polynomial R}
{a : R}
(a0 : a ≠ 0)
:
Polynomial.natDegree (Polynomial.C a * p) = Polynomial.natDegree p
@[simp]
theorem
Polynomial.nextCoeff_C_mul_X_add_C
{R : Type u}
[Semiring R]
{a : R}
(ha : a ≠ 0)
(c : R)
:
Polynomial.nextCoeff (Polynomial.C a * Polynomial.X + Polynomial.C c) = c
theorem
Polynomial.natDegree_comp
{R : Type u}
[Semiring R]
[NoZeroDivisors R]
{p : Polynomial R}
{q : Polynomial R}
:
@[simp]
theorem
Polynomial.natDegree_iterate_comp
{R : Type u}
[Semiring R]
[NoZeroDivisors R]
{p : Polynomial R}
{q : Polynomial R}
(k : ℕ)
:
Polynomial.natDegree ((Polynomial.comp p)^[k] q) = Polynomial.natDegree p ^ k * Polynomial.natDegree q
theorem
Polynomial.leadingCoeff_comp
{R : Type u}
[Semiring R]
[NoZeroDivisors R]
{p : Polynomial R}
{q : Polynomial R}
(hq : Polynomial.natDegree q ≠ 0)
:
Useful lemmas for the "monicization" of a nonzero polynomial p.
@[simp]
theorem
Polynomial.irreducible_mul_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
{p : Polynomial K}
:
Irreducible (p * Polynomial.C (Polynomial.leadingCoeff p)⁻¹) ↔ Irreducible p
@[simp]
theorem
Polynomial.dvd_mul_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
{p : Polynomial K}
{q : Polynomial K}
(hp0 : p ≠ 0)
:
theorem
Polynomial.monic_mul_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
{p : Polynomial K}
(h : p ≠ 0)
:
Polynomial.Monic (p * Polynomial.C (Polynomial.leadingCoeff p)⁻¹)
@[simp]
theorem
Polynomial.degree_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
{p : Polynomial K}
(hp0 : p ≠ 0)
:
Polynomial.degree (Polynomial.C (Polynomial.leadingCoeff p)⁻¹) = 0
theorem
Polynomial.degree_mul_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
{q : Polynomial K}
(h : q ≠ 0)
:
Polynomial.degree (p * Polynomial.C (Polynomial.leadingCoeff q)⁻¹) = Polynomial.degree p
theorem
Polynomial.natDegree_mul_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
{q : Polynomial K}
(h : q ≠ 0)
:
Polynomial.natDegree (p * Polynomial.C (Polynomial.leadingCoeff q)⁻¹) = Polynomial.natDegree p
theorem
Polynomial.degree_mul_leadingCoeff_self_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
:
Polynomial.degree (p * Polynomial.C (Polynomial.leadingCoeff p)⁻¹) = Polynomial.degree p
theorem
Polynomial.natDegree_mul_leadingCoeff_self_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
:
Polynomial.natDegree (p * Polynomial.C (Polynomial.leadingCoeff p)⁻¹) = Polynomial.natDegree p
@[simp]
theorem
Polynomial.degree_add_degree_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
:
Polynomial.degree p + Polynomial.degree (Polynomial.C (Polynomial.leadingCoeff p)⁻¹) = Polynomial.degree p