# mathlib3documentation

data.polynomial.div

# Division of univariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 {R : Type u} {f : polynomial R} :
f.coeff 0 = 0
theorem polynomial.X_pow_dvd_iff {R : Type u} {f : polynomial R} {n : } :
f (d : ), d < n f.coeff d = 0
theorem polynomial.multiplicity_finite_of_degree_pos_of_monic {R : Type u} {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 - * q).degree < p.degree
noncomputable def polynomial.div_mod_by_monic_aux {R : Type u} [ring R] (p : polynomial R) {q : polynomial R} :

See div_by_monic.

Equations
noncomputable def polynomial.div_by_monic {R : Type u} [ring R] (p q : polynomial R) :

div_by_monic gives the quotient of p by a monic polynomial q.

Equations
noncomputable def polynomial.mod_by_monic {R : Type u} [ring R] (p q : polynomial R) :

mod_by_monic gives the remainder of p by a monic polynomial q.

Equations
theorem polynomial.degree_mod_by_monic_lt {R : Type u} [ring R] [nontrivial R] (p : polynomial R) {q : polynomial R} (hq : q.monic) :
@[simp]
theorem polynomial.zero_mod_by_monic {R : Type u} [ring R] (p : polynomial R) :
0 %ₘ p = 0
@[simp]
theorem polynomial.zero_div_by_monic {R : Type u} [ring R] (p : polynomial R) :
0 /ₘ p = 0
@[simp]
theorem polynomial.mod_by_monic_zero {R : Type u} [ring R] (p : polynomial R) :
p %ₘ 0 = p
@[simp]
theorem polynomial.div_by_monic_zero {R : Type u} [ring R] (p : polynomial R) :
p /ₘ 0 = 0
theorem polynomial.div_by_monic_eq_of_not_monic {R : Type u} [ring R] {q : polynomial R} (p : polynomial R) (hq : ¬q.monic) :
p /ₘ q = 0
theorem polynomial.mod_by_monic_eq_of_not_monic {R : Type u} [ring R] {q : polynomial R} (p : polynomial R) (hq : ¬q.monic) :
p %ₘ q = p
theorem polynomial.mod_by_monic_eq_self_iff {R : Type u} [ring R] {p q : polynomial R} [nontrivial R] (hq : q.monic) :
p %ₘ q = p p.degree < q.degree
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) :
p %ₘ q = p - q * (p /ₘ q)
theorem polynomial.mod_by_monic_add_div {R : Type u} [comm_ring R] (p : polynomial R) {q : polynomial R} (hq : q.monic) :
p %ₘ q + q * (p /ₘ q) = p
theorem polynomial.div_by_monic_eq_zero_iff {R : Type u} [comm_ring R] {p q : polynomial R} [nontrivial R] (hq : q.monic) :
p /ₘ q = 0 p.degree < q.degree
theorem polynomial.degree_add_div_by_monic {R : Type u} [comm_ring R] {p q : polynomial R} (hq : q.monic) (h : q.degree p.degree) :
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) :
theorem polynomial.div_mod_by_monic_unique {R : Type u} [comm_ring R] {f g : polynomial R} (q r : polynomial R) (hg : g.monic) (h : r + g * q = f r.degree < g.degree) :
f /ₘ g = q f %ₘ g = r
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) :
(p /ₘ q) = /ₘ (p %ₘ 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) :
(p /ₘ 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) :
(p %ₘ q) = %ₘ
theorem polynomial.dvd_iff_mod_by_monic_eq_zero {R : Type u} [comm_ring R] {p q : polynomial R} (hq : q.monic) :
p %ₘ q = 0 q p
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) :
x y
@[simp]
theorem polynomial.mod_by_monic_one {R : Type u} [comm_ring R] (p : polynomial R) :
p %ₘ 1 = 0
@[simp]
theorem polynomial.div_by_monic_one {R : Type u} [comm_ring R] (p : polynomial R) :
p /ₘ 1 = p
@[simp]
theorem polynomial.mod_by_monic_X_sub_C_eq_C_eval {R : Type u} [comm_ring R] (p : polynomial R) (a : R) :
p %ₘ =
theorem polynomial.mul_div_by_monic_eq_iff_is_root {R : Type u} {a : R} [comm_ring R] {p : polynomial R} :
* (p /ₘ = p p.is_root a
theorem polynomial.dvd_iff_is_root {R : Type u} {a : R} [comm_ring R] {p : polynomial R} :
theorem polynomial.X_sub_C_dvd_sub_C_eval {R : Type u} {a : R} [comm_ring R] {p : polynomial R} :
p -
theorem polynomial.mod_by_monic_X {R : Type u} [comm_ring R] (p : polynomial R) :
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 : q = 0) :
(p %ₘ q) = 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) :
finset.univ.sum (λ (i : fin n), ((p %ₘ q).coeff i)) = p %ₘ q
theorem polynomial.sub_dvd_eval_sub {R : Type u} [comm_ring R] (a b : R) (p : polynomial R) :
a - b -
theorem polynomial.mul_div_mod_by_monic_cancel_left {R : Type u} [comm_ring R] (p : polynomial R) {q : polynomial R} (hmo : q.monic) :
q * p /ₘ q = p
theorem polynomial.ker_eval_ring_hom {R : Type u} [comm_ring R] (x : R) :
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
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
theorem polynomial.root_multiplicity_eq_multiplicity {R : Type u} [comm_ring R] (p : polynomial R) (a : R) :
= dite (p = 0) (λ (h0 : p = 0), 0) (λ (h0 : ¬p = 0), p).get _)
@[simp]
theorem polynomial.root_multiplicity_zero {R : Type u} [comm_ring R] {x : R} :
@[simp]
theorem polynomial.root_multiplicity_eq_zero_iff {R : Type u} [comm_ring R] {p : polynomial R} {x : R} :
p.is_root x p = 0
theorem polynomial.root_multiplicity_eq_zero {R : Type u} [comm_ring R] {p : polynomial R} {x : R} (h : ¬p.is_root x) :
@[simp]
theorem polynomial.root_multiplicity_pos' {R : Type u} [comm_ring R] {p : polynomial R} {x : R} :
p 0 p.is_root x
theorem polynomial.root_multiplicity_pos {R : Type u} [comm_ring R] {p : polynomial R} (hp : p 0) {x : R} :
@[simp]
theorem polynomial.root_multiplicity_C {R : Type u} [comm_ring R] (r a : R) :
theorem polynomial.pow_root_multiplicity_dvd {R : Type u} [comm_ring R] (p : polynomial R) (a : R) :