mathlib documentation

data.polynomial.div

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.

source
theorem polynomial.X_dvd_iff {α : Type u} [comm_semiring α] {f : α[X]} :
polynomial.X ∣ f ↔ f.coeff 0 = 0
source
theorem polynomial.multiplicity_finite_of_degree_pos_of_monic {R : Type u} [comm_semiring R] {p q : R[X]} (hp : 0 < p.degree) (hmp : p.monic) (hq : q ≠ 0) :
multiplicity.finite p q
source
theorem polynomial.div_wf_lemma {R : Type u} [ring R] {p q : R[X]} (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
source
noncomputable def polynomial.div_mod_by_monic_aux {R : Type u} [ring R] (p : R[X]) {q : R[X]} :
q.monic → R[X] × R[X]

See div_by_monic.

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

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

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

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

Equations
source
theorem polynomial.degree_mod_by_monic_lt {R : Type u} [ring R] [nontrivial R] (p : R[X]) {q : R[X]} (hq : q.monic) :
(p %ₘ q).degree < q.degree
source
@[simp]
theorem polynomial.zero_mod_by_monic {R : Type u} [ring R] (p : R[X]) :
0 %ₘ p = 0
source
@[simp]
theorem polynomial.zero_div_by_monic {R : Type u} [ring R] (p : R[X]) :
0 /ₘ p = 0
source
@[simp]
theorem polynomial.mod_by_monic_zero {R : Type u} [ring R] (p : R[X]) :
p %ₘ 0 = p
source
@[simp]
theorem polynomial.div_by_monic_zero {R : Type u} [ring R] (p : R[X]) :
p /ₘ 0 = 0
source
theorem polynomial.div_by_monic_eq_of_not_monic {R : Type u} [ring R] {q : R[X]} (p : R[X]) (hq : ¬q.monic) :
p /ₘ q = 0
source
theorem polynomial.mod_by_monic_eq_of_not_monic {R : Type u} [ring R] {q : R[X]} (p : R[X]) (hq : ¬q.monic) :
p %ₘ q = p
source
theorem polynomial.mod_by_monic_eq_self_iff {R : Type u} [ring R] {p q : R[X]} [nontrivial R] (hq : q.monic) :
p %ₘ q = p ↔ p.degree < q.degree
source
theorem polynomial.degree_mod_by_monic_le {R : Type u} [ring R] (p : R[X]) {q : R[X]} (hq : q.monic) :
(p %ₘ q).degree ≤ q.degree
source
theorem polynomial.mod_by_monic_eq_sub_mul_div {R : Type u} [comm_ring R] (p : R[X]) {q : R[X]} (hq : q.monic) :
p %ₘ q = p - q * (p /ₘ q)
source
theorem polynomial.mod_by_monic_add_div {R : Type u} [comm_ring R] (p : R[X]) {q : R[X]} (hq : q.monic) :
p %ₘ q + q * (p /ₘ q) = p
source
theorem polynomial.div_by_monic_eq_zero_iff {R : Type u} [comm_ring R] {p q : R[X]} [nontrivial R] (hq : q.monic) :
p /ₘ q = 0 ↔ p.degree < q.degree
source
theorem polynomial.degree_add_div_by_monic {R : Type u} [comm_ring R] {p q : R[X]} (hq : q.monic) (h : q.degree ≤ p.degree) :
q.degree + (p /ₘ q).degree = p.degree
source
theorem polynomial.degree_div_by_monic_le {R : Type u} [comm_ring R] (p q : R[X]) :
(p /ₘ q).degree ≤ p.degree
source
theorem polynomial.degree_div_by_monic_lt {R : Type u} [comm_ring R] (p : R[X]) {q : R[X]} (hq : q.monic) (hp0 : p ≠ 0) (h0q : 0 < q.degree) :
(p /ₘ q).degree < p.degree
source
theorem polynomial.nat_degree_div_by_monic {R : Type u} [comm_ring R] (f : R[X]) {g : R[X]} (hg : g.monic) :
(f /ₘ g).nat_degree = f.nat_degree - g.nat_degree
source
theorem polynomial.div_mod_by_monic_unique {R : Type u} [comm_ring R] {f g : R[X]} (q r : R[X]) (hg : g.monic) (h : r + g * q = f ∧ r.degree < g.degree) :
f /ₘ g = q ∧ f %ₘ g = r
source
theorem polynomial.map_mod_div_by_monic {R : Type u} {S : Type v} [comm_ring R] {p q : R[X]} [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
source
theorem polynomial.map_div_by_monic {R : Type u} {S : Type v} [comm_ring R] {p q : R[X]} [comm_ring S] (f : R →+* S) (hq : q.monic) :
polynomial.map f (p /ₘ q) = polynomial.map f p /ₘ polynomial.map f q
source
theorem polynomial.map_mod_by_monic {R : Type u} {S : Type v} [comm_ring R] {p q : R[X]} [comm_ring S] (f : R →+* S) (hq : q.monic) :
polynomial.map f (p %ₘ q) = polynomial.map f p %ₘ polynomial.map f q
source
theorem polynomial.dvd_iff_mod_by_monic_eq_zero {R : Type u} [comm_ring R] {p q : R[X]} (hq : q.monic) :
p %ₘ q = 0 ↔ q ∣ p
source
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 : R[X]} (hx : x.monic) :
polynomial.map f x ∣ polynomial.map f y ↔ x ∣ y
source
@[simp]
theorem polynomial.mod_by_monic_one {R : Type u} [comm_ring R] (p : R[X]) :
p %ₘ 1 = 0
source
@[simp]
theorem polynomial.div_by_monic_one {R : Type u} [comm_ring R] (p : R[X]) :
p /ₘ 1 = p
source
@[simp]
theorem polynomial.mod_by_monic_X_sub_C_eq_C_eval {R : Type u} [comm_ring R] (p : R[X]) (a : R) :
p %ₘ (polynomial.X - ⇑polynomial.C a) = ⇑polynomial.C (polynomial.eval a p)
source
theorem polynomial.mul_div_by_monic_eq_iff_is_root {R : Type u} {a : R} [comm_ring R] {p : R[X]} :
(polynomial.X - ⇑polynomial.C a) * (p /ₘ (polynomial.X - ⇑polynomial.C a)) = p ↔ p.is_root a
source
theorem polynomial.dvd_iff_is_root {R : Type u} {a : R} [comm_ring R] {p : R[X]} :
polynomial.X - ⇑polynomial.C a ∣ p ↔ p.is_root a
source
theorem polynomial.mod_by_monic_X {R : Type u} [comm_ring R] (p : R[X]) :
p %ₘ polynomial.X = ⇑polynomial.C (polynomial.eval 0 p)
source
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 : R[X]} (hq : q.monic) {x : S} (hx : polynomial.eval₂ f x q = 0) :
polynomial.eval₂ f x (p %ₘ q) = polynomial.eval₂ f x p
source
theorem polynomial.sum_mod_by_monic_coeff {R : Type u} [comm_ring R] {p q : R[X]} (hq : q.monic) {n : ℕ} (hn : q.degree ≤ ↑n) :
∑ (i : fin n), ⇑(polynomial.monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q
source
theorem polynomial.sub_dvd_eval_sub {R : Type u} [comm_ring R] (a b : R) (p : R[X]) :
a - b ∣ polynomial.eval a p - polynomial.eval b p
source
theorem polynomial.not_is_field (R : Type u) [comm_ring R] :
¬is_field R[X]
source
noncomputable def polynomial.decidable_dvd_monic {R : Type u} [comm_ring R] {q : R[X]} (p : R[X]) (hq : q.monic) :
decidable (q ∣ p)

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
source
theorem polynomial.multiplicity_X_sub_C_finite {R : Type u} [comm_ring R] {p : R[X]} (a : R) (h0 : p ≠ 0) :
multiplicity.finite (polynomial.X - ⇑polynomial.C a) p
source
noncomputable def polynomial.root_multiplicity {R : Type u} [comm_ring R] (a : R) (p : R[X]) :
ℕ

The largest power of X - C a which divides p. This is computable via the divisibility algorithm decidable_dvd_monic.

Equations
source
theorem polynomial.root_multiplicity_eq_multiplicity {R : Type u} [comm_ring R] (p : R[X]) (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 _)
source
@[simp]
theorem polynomial.root_multiplicity_zero {R : Type u} [comm_ring R] {x : R} :
polynomial.root_multiplicity x 0 = 0
source
theorem polynomial.root_multiplicity_eq_zero {R : Type u} [comm_ring R] {p : R[X]} {x : R} (h : ¬p.is_root x) :
polynomial.root_multiplicity x p = 0
source
theorem polynomial.root_multiplicity_pos {R : Type u} [comm_ring R] {p : R[X]} (hp : p ≠ 0) {x : R} :
0 < polynomial.root_multiplicity x p ↔ p.is_root x
source
@[simp]
theorem polynomial.root_multiplicity_C {R : Type u} [comm_ring R] (r a : R) :
polynomial.root_multiplicity a (⇑polynomial.C r) = 0
source
theorem polynomial.pow_root_multiplicity_dvd {R : Type u} [comm_ring R] (p : R[X]) (a : R) :
(polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p ∣ p
source
theorem polynomial.div_by_monic_mul_pow_root_multiplicity_eq {R : Type u} [comm_ring R] (p : R[X]) (a : R) :
(p /ₘ (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p) * (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p = p
source
theorem polynomial.eval_div_by_monic_pow_root_multiplicity_ne_zero {R : Type u} [comm_ring R] {p : R[X]} (a : R) (hp : p ≠ 0) :
polynomial.eval a (p /ₘ (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p) ≠ 0