# mathlibdocumentation

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.

def polynomial.coeff_coe_to_fun {R : Type u} [semiring R] :

The coercion turning a polynomial into the function which reports the coefficient of a given monomial X^n

Equations
theorem polynomial.apply_eq_coeff {R : Type u} {n : } [semiring R] {p : polynomial R} :
p n = p.coeff n

def polynomial.div_X {R : Type u} [semiring R] :

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

Equations
theorem polynomial.div_X_mul_X_add {R : Type u} [semiring R] (p : polynomial R) :

@[simp]
theorem polynomial.div_X_C {R : Type u} [semiring R] (a : R) :
.div_X = 0

theorem polynomial.div_X_eq_zero_iff {R : Type u} [semiring R] {p : polynomial R} :

theorem polynomial.div_X_add {R : Type u} [semiring R] {p q : polynomial R} :
(p + q).div_X = p.div_X + q.div_X

theorem polynomial.degree_div_X_lt {R : Type u} [semiring R] {p : polynomial R} :
p 0p.div_X.degree < p.degree

def polynomial.rec_on_horner {R : Type u} [semiring R] {M : Sort u_1} (p : polynomial R) :
M 0(Π (p : (a : R), p.coeff 0 = 0a 0M pM (p + (Π (p : , p 0M pM (p * polynomial.X))M p

An induction principle for polynomials, valued in Sort* instead of Prop.

Equations
theorem polynomial.degree_pos_induction_on {R : Type u} [semiring R] {P : → Prop} (p : polynomial R) :
0 < p.degree(∀ {a : R}, a 0P ((polynomial.C a) * polynomial.X))(∀ {p : , 0 < p.degreeP pP (p * polynomial.X))(∀ {p : {a : R}, 0 < p.degreeP pP (p + P p

theorem polynomial.X_dvd_iff {α : Type u} {f : polynomial α} :
f.coeff 0 = 0

theorem polynomial.multiplicity_finite_of_degree_pos_of_monic {R : Type u} {p q : polynomial R} :
0 < p.degreep.monicq 0

theorem polynomial.div_wf_lemma {R : Type u} [ring R] {p q : polynomial R} :

def polynomial.div_mod_by_monic_aux {R : Type u} [ring R] (p : polynomial R) {q : polynomial R} :
q.monic

See div_by_monic.

Equations
def polynomial.div_by_monic {R : Type u} [ring R] :

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

Equations
def polynomial.mod_by_monic {R : Type u} [ring 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] (p : polynomial R) {q : polynomial R} :
q.monicq 0(p %ₘ q).degree < q.degree

@[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) :
¬q.monicp /ₘ q = 0

theorem polynomial.mod_by_monic_eq_of_not_monic {R : Type u} [ring R] {q : polynomial R} (p : polynomial R) :
¬q.monicp %ₘ q = p

theorem polynomial.mod_by_monic_eq_self_iff {R : Type u} [ring R] {p q : polynomial R} :
q.monicq 0(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} :
q.monic(p %ₘ q).degree q.degree

theorem polynomial.mod_by_monic_eq_sub_mul_div {R : Type u} [comm_ring R] (p : polynomial R) {q : polynomial R} :
q.monicp %ₘ q = p - q * (p /ₘ q)

theorem polynomial.mod_by_monic_add_div {R : Type u} [comm_ring R] (p : polynomial R) {q : polynomial R} :
q.monicp %ₘ q + q * (p /ₘ q) = p

theorem polynomial.div_by_monic_eq_zero_iff {R : Type u} [comm_ring R] {p q : polynomial R} :
q.monicq 0(p /ₘ q = 0 p.degree < q.degree)

theorem polynomial.degree_add_div_by_monic {R : Type u} [comm_ring R] {p q : polynomial R} :
q.monicq.degree p.degreeq.degree + (p /ₘ q).degree = p.degree

theorem polynomial.degree_div_by_monic_le {R : Type u} [comm_ring R] (p q : polynomial R) :

theorem polynomial.degree_div_by_monic_lt {R : Type u} [comm_ring R] (p : polynomial R) {q : polynomial R} :
q.monicp 00 < q.degree(p /ₘ q).degree < p.degree

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 =

theorem polynomial.div_mod_by_monic_unique {R : Type u} [comm_ring R] {f g : polynomial R} (q r : polynomial R) :
g.monicr + g * q = f r.degree < g.degreef /ₘ 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) :
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) :
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) :
q.monic (p %ₘ q) = %ₘ

theorem polynomial.dvd_iff_mod_by_monic_eq_zero {R : Type u} [comm_ring R] {p q : polynomial R} :
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} :
x.monic x 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.mod_by_monic_X {R : Type u} [comm_ring R] (p : polynomial R) :

def polynomial.decidable_dvd_monic {R : Type u} [comm_ring R] {q : polynomial R} (p : polynomial R) :
q.monicdecidable (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
theorem polynomial.multiplicity_X_sub_C_finite {R : Type u} [comm_ring R] {p : polynomial R} (a : R) :
p 0

def polynomial.root_multiplicity {R : Type u} [comm_ring R] :
R →

The largest power of X - C a which divides p. This is computable via the divisibility algorithm 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 _)

theorem polynomial.pow_root_multiplicity_dvd {R : Type u} [comm_ring R] (p : polynomial R) (a : R) :

theorem polynomial.div_by_monic_mul_pow_root_multiplicity_eq {R : Type u} [comm_ring R] (p : polynomial R) (a : R) :
(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 (p /ₘ 0