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.
The coercion turning a polynomial into the function which reports the coefficient of a given
monomial X^n
div_X p return a polynomial q such that q * X + C (p.coeff 0) = p.
It can be used in a semiring where the usual division algorithm is not possible
theorem
polynomial.div_X_mul_X_add
{R : Type u}
[semiring R]
(p : polynomial R) :
p.div_X * polynomial.X + ⇑polynomial.C (p.coeff 0) = p
@[simp]
def
polynomial.rec_on_horner
{R : Type u}
[semiring R]
{M : polynomial R → Sort u_1}
(p : polynomial R) :
M 0 → (Π (p : polynomial R) (a : R), p.coeff 0 = 0 → a ≠ 0 → M p → M (p + ⇑polynomial.C a)) → (Π (p : polynomial R), p ≠ 0 → M p → M (p * polynomial.X)) → M p
An induction principle for polynomials, valued in Sort* instead of Prop.
Equations
- p.rec_on_horner = λ (M0 : M 0) (MC : Π (p : polynomial R) (a : R), p.coeff 0 = 0 → a ≠ 0 → M p → M (p + ⇑polynomial.C a)) (MX : Π (p : polynomial R), p ≠ 0 → M p → M (p * polynomial.X)), dite (p = 0) (λ (hp : p = 0), _.rec_on M0) (λ (hp : ¬p = 0), _.mpr (dite (p.coeff 0 = 0) (λ (hcp0 : p.coeff 0 = 0), _.mpr (_.mpr (_.mpr (MX p.div_X _ (p.div_X.rec_on_horner M0 MC MX))))) (λ (hcp0 : ¬p.coeff 0 = 0), MC (p.div_X * polynomial.X) (p.coeff 0) _ hcp0 (dite (p.div_X = 0) (λ (hpX0 : p.div_X = 0), show M (p.div_X * polynomial.X), from _.mpr (polynomial.rec_on_horner._main._pack._proof_9.mpr M0)) (λ (hpX0 : ¬p.div_X = 0), MX p.div_X hpX0 (p.div_X.rec_on_horner M0 MC MX))))))
theorem
polynomial.degree_pos_induction_on
{R : Type u}
[semiring R]
{P : polynomial R → Prop}
(p : polynomial R) :
0 < p.degree → (∀ {a : R}, a ≠ 0 → P (⇑polynomial.C a * polynomial.X)) → (∀ {p : polynomial R}, 0 < p.degree → P p → P (p * polynomial.X)) → (∀ {p : polynomial R} {a : R}, 0 < p.degree → P p → P (p + ⇑polynomial.C a)) → P p
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} :
0 < p.degree → p.monic → q ≠ 0 → multiplicity.finite p q
theorem
polynomial.div_wf_lemma
{R : Type u}
[ring R]
{p q : polynomial R} :
q.degree ≤ p.degree ∧ p ≠ 0 → q.monic → (p - ⇑polynomial.C p.leading_coeff * polynomial.X ^ (p.nat_degree - q.nat_degree) * q).degree < p.degree
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]
(p : polynomial R)
{q : polynomial R} :
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.div_by_monic_eq_of_not_monic
{R : Type u}
[ring R]
{q : polynomial R}
(p : polynomial R) :
theorem
polynomial.mod_by_monic_eq_of_not_monic
{R : Type u}
[ring R]
{q : polynomial R}
(p : polynomial R) :
theorem
polynomial.degree_mod_by_monic_le
{R : Type u}
[ring R]
(p : polynomial R)
{q : polynomial R} :
theorem
polynomial.mod_by_monic_eq_sub_mul_div
{R : Type u}
[comm_ring R]
(p : polynomial R)
{q : polynomial R} :
theorem
polynomial.mod_by_monic_add_div
{R : Type u}
[comm_ring R]
(p : polynomial R)
{q : polynomial R} :
theorem
polynomial.degree_div_by_monic_lt
{R : Type u}
[comm_ring R]
(p : polynomial R)
{q : polynomial R} :
theorem
polynomial.nat_degree_div_by_monic
{R : Type u}
[comm_ring R]
(f : polynomial R)
{g : polynomial R} :
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) :
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) :
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) :
q.monic → polynomial.map f (p %ₘ q) = polynomial.map f p %ₘ polynomial.map f q
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} :
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)
def
polynomial.decidable_dvd_monic
{R : Type u}
[comm_ring R]
{q : polynomial R}
(p : polynomial R) :
An algorithm for deciding polynomial divisibility.
The algorithm is "compute p %ₘ q and compare to 0".
Seepolynomial.mod_by_monicfor 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) :
p ≠ 0 → multiplicity.finite (polynomial.X - ⇑polynomial.C a) p
The largest power of X - C a which divides p.
This is computable via the divisibility algorithm 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 _)
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) :
p ≠ 0 → polynomial.eval a (p /ₘ (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p) ≠ 0