Division of univariate polynomials #
The main defs are div_by_monic
and mod_by_monic
.
The compatibility between these is given by mod_by_monic_add_div
.
We also define root_multiplicity
.
theorem
polynomial.X_dvd_iff
{α : Type u}
[comm_semiring α]
{f : polynomial α} :
polynomial.X ∣ f ↔ f.coeff 0 = 0
theorem
polynomial.multiplicity_finite_of_degree_pos_of_monic
{R : Type u}
[comm_semiring R]
{p q : polynomial R}
(hp : 0 < p.degree)
(hmp : p.monic)
(hq : q ≠ 0) :
theorem
polynomial.div_wf_lemma
{R : Type u}
[ring R]
{p q : polynomial R}
(h : q.degree ≤ p.degree ∧ p ≠ 0)
(hq : q.monic) :
(p - ⇑polynomial.C p.leading_coeff * polynomial.X ^ (p.nat_degree - q.nat_degree) * q).degree < p.degree
noncomputable
def
polynomial.div_mod_by_monic_aux
{R : Type u}
[ring R]
(p : polynomial R)
{q : polynomial R} :
q.monic → polynomial R × polynomial R
See div_by_monic
.
Equations
- p.div_mod_by_monic_aux = λ (q : polynomial R) (hq : q.monic), ite (q.degree ≤ p.degree ∧ p ≠ 0) (let z : polynomial R := ⇑polynomial.C p.leading_coeff * polynomial.X ^ (p.nat_degree - q.nat_degree) in let dm : polynomial R × polynomial R := (p - z * q).div_mod_by_monic_aux hq in (z + dm.fst, dm.snd)) (0, p)
div_by_monic
gives the quotient of p
by a monic polynomial q
.
mod_by_monic
gives the remainder of p
by a monic polynomial q
.
theorem
polynomial.degree_mod_by_monic_lt
{R : Type u}
[ring R]
[nontrivial R]
(p : polynomial R)
{q : polynomial R}
(hq : q.monic) :
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.div_by_monic_eq_of_not_monic
{R : Type u}
[ring R]
{q : polynomial R}
(p : polynomial R)
(hq : ¬q.monic) :
theorem
polynomial.mod_by_monic_eq_of_not_monic
{R : Type u}
[ring R]
{q : polynomial R}
(p : polynomial R)
(hq : ¬q.monic) :
theorem
polynomial.mod_by_monic_eq_self_iff
{R : Type u}
[ring R]
{p q : polynomial R}
[nontrivial R]
(hq : q.monic) :
theorem
polynomial.degree_mod_by_monic_le
{R : Type u}
[ring R]
(p : polynomial R)
{q : polynomial R}
(hq : q.monic) :
theorem
polynomial.mod_by_monic_eq_sub_mul_div
{R : Type u}
[comm_ring R]
(p : polynomial R)
{q : polynomial R}
(hq : q.monic) :
theorem
polynomial.mod_by_monic_add_div
{R : Type u}
[comm_ring R]
(p : polynomial R)
{q : polynomial R}
(hq : q.monic) :
theorem
polynomial.div_by_monic_eq_zero_iff
{R : Type u}
[comm_ring R]
{p q : polynomial R}
[nontrivial R]
(hq : q.monic) :
theorem
polynomial.degree_div_by_monic_lt
{R : Type u}
[comm_ring R]
(p : polynomial R)
{q : polynomial R}
(hq : q.monic)
(hp0 : p ≠ 0)
(h0q : 0 < q.degree) :
theorem
polynomial.nat_degree_div_by_monic
{R : Type u}
[comm_ring R]
(f : polynomial R)
{g : polynomial R}
(hg : g.monic) :
(f /ₘ g).nat_degree = f.nat_degree - g.nat_degree
theorem
polynomial.map_mod_div_by_monic
{R : Type u}
{S : Type v}
[comm_ring R]
{p q : polynomial R}
[comm_ring S]
(f : R →+* S)
(hq : q.monic) :
polynomial.map f (p /ₘ q) = polynomial.map f p /ₘ polynomial.map f q ∧ polynomial.map f (p %ₘ q) = polynomial.map f p %ₘ polynomial.map f q
theorem
polynomial.map_div_by_monic
{R : Type u}
{S : Type v}
[comm_ring R]
{p q : polynomial R}
[comm_ring S]
(f : R →+* S)
(hq : q.monic) :
polynomial.map f (p /ₘ q) = polynomial.map f p /ₘ polynomial.map f q
theorem
polynomial.map_mod_by_monic
{R : Type u}
{S : Type v}
[comm_ring R]
{p q : polynomial R}
[comm_ring S]
(f : R →+* S)
(hq : q.monic) :
polynomial.map f (p %ₘ q) = polynomial.map f p %ₘ polynomial.map f q
theorem
polynomial.dvd_iff_mod_by_monic_eq_zero
{R : Type u}
[comm_ring R]
{p q : polynomial R}
(hq : q.monic) :
theorem
polynomial.map_dvd_map
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.injective ⇑f)
{x y : polynomial R}
(hx : x.monic) :
polynomial.map f x ∣ polynomial.map f y ↔ x ∣ y
@[simp]
@[simp]
@[simp]
theorem
polynomial.mod_by_monic_X_sub_C_eq_C_eval
{R : Type u}
[comm_ring R]
(p : polynomial R)
(a : R) :
p %ₘ (polynomial.X - ⇑polynomial.C a) = ⇑polynomial.C (polynomial.eval a p)
theorem
polynomial.mul_div_by_monic_eq_iff_is_root
{R : Type u}
{a : R}
[comm_ring R]
{p : polynomial R} :
(polynomial.X - ⇑polynomial.C a) * (p /ₘ (polynomial.X - ⇑polynomial.C a)) = p ↔ p.is_root a
theorem
polynomial.dvd_iff_is_root
{R : Type u}
{a : R}
[comm_ring R]
{p : polynomial R} :
polynomial.X - ⇑polynomial.C a ∣ p ↔ p.is_root a
theorem
polynomial.mod_by_monic_X
{R : Type u}
[comm_ring R]
(p : polynomial R) :
p %ₘ polynomial.X = ⇑polynomial.C (polynomial.eval 0 p)
theorem
polynomial.eval₂_mod_by_monic_eq_self_of_root
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{f : R →+* S}
{p q : polynomial R}
(hq : q.monic)
{x : S}
(hx : polynomial.eval₂ f x q = 0) :
polynomial.eval₂ f x (p %ₘ q) = polynomial.eval₂ f x p
theorem
polynomial.sum_mod_by_monic_coeff
{R : Type u}
[comm_ring R]
{p q : polynomial R}
(hq : q.monic)
{n : ℕ}
(hn : q.degree ≤ ↑n) :
theorem
polynomial.sub_dvd_eval_sub
{R : Type u}
[comm_ring R]
(a b : R)
(p : polynomial R) :
a - b ∣ polynomial.eval a p - polynomial.eval b p
noncomputable
def
polynomial.decidable_dvd_monic
{R : Type u}
[comm_ring R]
{q : polynomial R}
(p : polynomial R)
(hq : q.monic) :
An algorithm for deciding polynomial divisibility.
The algorithm is "compute p %ₘ q
and compare to 0
".
See polynomial.mod_by_monic
for the algorithm that computes %ₘ
.
Equations
- p.decidable_dvd_monic hq = decidable_of_iff (p %ₘ q = 0) _
theorem
polynomial.multiplicity_X_sub_C_finite
{R : Type u}
[comm_ring R]
{p : polynomial R}
(a : R)
(h0 : p ≠ 0) :
noncomputable
def
polynomial.root_multiplicity
{R : Type u}
[comm_ring R]
(a : R)
(p : polynomial R) :
The largest power of X - C a
which divides p
.
This is computable via the divisibility algorithm polynomial.decidable_dvd_monic
.
Equations
- polynomial.root_multiplicity a p = dite (p = 0) (λ (h0 : p = 0), 0) (λ (h0 : ¬p = 0), let I : decidable_pred (λ (n : ℕ), ¬(polynomial.X - ⇑polynomial.C a) ^ (n + 1) ∣ p) := λ (n : ℕ), not.decidable in nat.find _)
theorem
polynomial.root_multiplicity_eq_multiplicity
{R : Type u}
[comm_ring R]
(p : polynomial R)
(a : R) :
polynomial.root_multiplicity a p = dite (p = 0) (λ (h0 : p = 0), 0) (λ (h0 : ¬p = 0), (multiplicity (polynomial.X - ⇑polynomial.C a) p).get _)
@[simp]
theorem
polynomial.root_multiplicity_eq_zero
{R : Type u}
[comm_ring R]
{p : polynomial R}
{x : R}
(h : ¬p.is_root x) :
theorem
polynomial.root_multiplicity_pos
{R : Type u}
[comm_ring R]
{p : polynomial R}
(hp : p ≠ 0)
{x : R} :
0 < polynomial.root_multiplicity x p ↔ p.is_root x
@[simp]
theorem
polynomial.pow_root_multiplicity_dvd
{R : Type u}
[comm_ring R]
(p : polynomial R)
(a : R) :
(polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p ∣ p
theorem
polynomial.div_by_monic_mul_pow_root_multiplicity_eq
{R : Type u}
[comm_ring R]
(p : polynomial R)
(a : R) :
p /ₘ (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p * (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p = p
theorem
polynomial.eval_div_by_monic_pow_root_multiplicity_ne_zero
{R : Type u}
[comm_ring R]
{p : polynomial R}
(a : R)
(hp : p ≠ 0) :
polynomial.eval a (p /ₘ (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p) ≠ 0