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.natDegree_comp_eq_of_mul_ne_zero
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0)
:
theorem
Polynomial.degree_pos_of_root
{R : Type u}
{a : R}
[Semiring R]
{p : Polynomial R}
(hp : p ≠ 0)
(h : p.IsRoot a)
:
0 < p.degree
theorem
Polynomial.natDegree_add_le_iff_left
{R : Type u}
[Semiring R]
{n : ℕ}
(p : Polynomial R)
(q : Polynomial R)
(qn : q.natDegree ≤ n)
:
theorem
Polynomial.natDegree_add_le_iff_right
{R : Type u}
[Semiring R]
{n : ℕ}
(p : Polynomial R)
(q : Polynomial R)
(pn : p.natDegree ≤ n)
:
theorem
Polynomial.eq_natDegree_of_le_mem_support
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
(pn : p.natDegree ≤ n)
(ns : n ∈ p.support)
:
p.natDegree = n
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)
:
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)
:
theorem
Polynomial.natDegree_mul_C_eq_of_mul_ne_zero
{R : Type u}
{a : R}
[Semiring R]
{p : Polynomial R}
(h : p.leadingCoeff * a ≠ 0)
:
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 * p.leadingCoeff ≠ 0)
:
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)
:
theorem
Polynomial.natDegree_lt_coeff_mul
{R : Type u}
{m : ℕ}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(h : p.natDegree + q.natDegree < m + n)
:
theorem
Polynomial.coeff_mul_of_natDegree_le
{R : Type u}
{m : ℕ}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(pm : p.natDegree ≤ m)
(qn : q.natDegree ≤ n)
:
theorem
Polynomial.coeff_add_eq_left_of_lt
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(qn : q.natDegree < n)
:
theorem
Polynomial.coeff_add_eq_right_of_lt
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(pn : p.natDegree < n)
:
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)
:
0 < p.natDegree
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 < p.degree
@[simp]
@[simp]
theorem
Polynomial.degree_map_eq_iff
{R : Type u}
{S : Type v}
[Semiring R]
[Semiring S]
{f : R →+* S}
{p : Polynomial R}
:
@[simp]
theorem
Polynomial.natDegree_map_eq_iff
{R : Type u}
{S : Type v}
[Semiring R]
[Semiring S]
{f : R →+* S}
{p : Polynomial R}
:
theorem
Polynomial.natDegree_pos_of_nextCoeff_ne_zero
{R : Type u}
[Semiring R]
{p : Polynomial R}
(h : p.nextCoeff ≠ 0)
:
0 < p.natDegree
theorem
Polynomial.natDegree_sub_le_iff_left
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(qn : q.natDegree ≤ n)
:
theorem
Polynomial.natDegree_sub_le_iff_right
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(pn : p.natDegree ≤ n)
:
theorem
Polynomial.coeff_sub_eq_left_of_lt
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(dg : q.natDegree < n)
:
theorem
Polynomial.coeff_sub_eq_neg_right_of_lt
{R : Type u}
{n : ℕ}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(df : p.natDegree < n)
:
theorem
Polynomial.degree_mul_C
{R : Type u}
[Semiring R]
{p : Polynomial R}
{a : R}
[NoZeroDivisors R]
(a0 : a ≠ 0)
:
theorem
Polynomial.degree_C_mul
{R : Type u}
[Semiring R]
{p : Polynomial R}
{a : R}
[NoZeroDivisors R]
(a0 : a ≠ 0)
:
theorem
Polynomial.natDegree_mul_C
{R : Type u}
[Semiring R]
{p : Polynomial R}
{a : R}
[NoZeroDivisors R]
(a0 : a ≠ 0)
:
theorem
Polynomial.natDegree_C_mul
{R : Type u}
[Semiring R]
{p : Polynomial R}
{a : R}
[NoZeroDivisors R]
(a0 : a ≠ 0)
:
theorem
Polynomial.natDegree_comp
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
[NoZeroDivisors R]
:
@[simp]
theorem
Polynomial.natDegree_iterate_comp
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
[NoZeroDivisors R]
(k : ℕ)
:
theorem
Polynomial.leadingCoeff_comp
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
[NoZeroDivisors R]
(hq : q.natDegree ≠ 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 p.leadingCoeff⁻¹) ↔ 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)
:
@[simp]
theorem
Polynomial.degree_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
{p : Polynomial K}
(hp0 : p ≠ 0)
:
theorem
Polynomial.degree_mul_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
{q : Polynomial K}
(h : q ≠ 0)
:
theorem
Polynomial.natDegree_mul_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
{q : Polynomial K}
(h : q ≠ 0)
:
theorem
Polynomial.degree_mul_leadingCoeff_self_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
:
theorem
Polynomial.natDegree_mul_leadingCoeff_self_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
:
@[simp]
theorem
Polynomial.degree_add_degree_leadingCoeff_inv
{K : Type u_1}
[DivisionRing K]
(p : Polynomial K)
: