Division of univariate polynomials

The main defs are divByMonic and modByMonic. The compatibility between these is given by modByMonic_add_div. We also define rootMultiplicity.

theorem Polynomial.X_dvd_iff {R : Type u} [Semiring R] {f : Polynomial R} : Polynomial.X ∣ f ↔ Polynomial.coeff f 0 = 0

theorem Polynomial.X_pow_dvd_iff {R : Type u} [Semiring R] {f : Polynomial R} {n : ℕ} : Polynomial.X ^ n ∣ f ↔ ∀ d < n, Polynomial.coeff f d = 0

theorem Polynomial.multiplicity_finite_of_degree_pos_of_monic {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : 0 < Polynomial.degree p) (hmp : Polynomial.Monic p) (hq : q ≠ 0) : multiplicity.Finite p q

theorem Polynomial.div_wf_lemma {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} (h : Polynomial.degree q ≤ Polynomial.degree p ∧ p ≠ 0) (hq : Polynomial.Monic q) : Polynomial.degree (p - q * (Polynomial.C (Polynomial.leadingCoeff p) * Polynomial.X ^ (Polynomial.natDegree p - Polynomial.natDegree q))) < Polynomial.degree p

noncomputable def Polynomial.divModByMonicAux {R : Type u} [Ring R] (_p : Polynomial R) {q : Polynomial R} : Polynomial.Monic q → Polynomial R × Polynomial R

See divByMonic.

Equations

• One or more equations did not get rendered due to their size.

def Polynomial.divByMonic {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) : Polynomial R

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

Equations

• p /ₘ q = if hq : Polynomial.Monic q then (Polynomial.divModByMonicAux p hq).1 else 0

def Polynomial.modByMonic {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) : Polynomial R

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

Equations

• p %ₘ q = if hq : Polynomial.Monic q then (Polynomial.divModByMonicAux p hq).2 else p

def Polynomial.«term_/ₘ_» : Lean.TrailingParserDescr

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

Equations

• Polynomial.«term_/ₘ_» = Lean.ParserDescr.trailingNode `Polynomial.term_/ₘ_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /ₘ ") (Lean.ParserDescr.cat `term 71))

def Polynomial.«term_%ₘ_» : Lean.TrailingParserDescr

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

Equations

• Polynomial.«term_%ₘ_» = Lean.ParserDescr.trailingNode `Polynomial.term_%ₘ_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " %ₘ ") (Lean.ParserDescr.cat `term 71))

theorem Polynomial.degree_modByMonic_lt {R : Type u} [Ring R] [Nontrivial R] (p : Polynomial R) {q : Polynomial R} (_hq : Polynomial.Monic q) : Polynomial.degree (p %ₘ q) < Polynomial.degree q

theorem Polynomial.natDegree_modByMonic_lt {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmq : Polynomial.Monic q) (hq : q ≠ 1) : Polynomial.natDegree (p %ₘ q) < Polynomial.natDegree q

@[simp]

theorem Polynomial.zero_modByMonic {R : Type u} [Ring R] (p : Polynomial R) : 0 %ₘ p = 0

@[simp]

theorem Polynomial.zero_divByMonic {R : Type u} [Ring R] (p : Polynomial R) : 0 /ₘ p = 0

@[simp]

theorem Polynomial.modByMonic_zero {R : Type u} [Ring R] (p : Polynomial R) : p %ₘ 0 = p

@[simp]

theorem Polynomial.divByMonic_zero {R : Type u} [Ring R] (p : Polynomial R) : p /ₘ 0 = 0

theorem Polynomial.divByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬Polynomial.Monic q) : p /ₘ q = 0

theorem Polynomial.modByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬Polynomial.Monic q) : p %ₘ q = p

theorem Polynomial.modByMonic_eq_self_iff {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} [Nontrivial R] (hq : Polynomial.Monic q) : p %ₘ q = p ↔ Polynomial.degree p < Polynomial.degree q

theorem Polynomial.degree_modByMonic_le {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : Polynomial.Monic q) : Polynomial.degree (p %ₘ q) ≤ Polynomial.degree q

theorem Polynomial.natDegree_modByMonic_le {R : Type u} [Ring R] (p : Polynomial R) {g : Polynomial R} (hg : Polynomial.Monic g) : Polynomial.natDegree (p %ₘ g) ≤ Polynomial.natDegree g

theorem Polynomial.X_dvd_sub_C {R : Type u} [Ring R] {p : Polynomial R} : Polynomial.X ∣ p - Polynomial.C (Polynomial.coeff p 0)

theorem Polynomial.modByMonic_eq_sub_mul_div {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (_hq : Polynomial.Monic q) : p %ₘ q = p - q * (p /ₘ q)

theorem Polynomial.modByMonic_add_div {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : Polynomial.Monic q) : p %ₘ q + q * (p /ₘ q) = p

theorem Polynomial.divByMonic_eq_zero_iff {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} [Nontrivial R] (hq : Polynomial.Monic q) : p /ₘ q = 0 ↔ Polynomial.degree p < Polynomial.degree q

theorem Polynomial.degree_add_divByMonic {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) (h : Polynomial.degree q ≤ Polynomial.degree p) : Polynomial.degree q + Polynomial.degree (p /ₘ q) = Polynomial.degree p

theorem Polynomial.degree_divByMonic_le {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) : Polynomial.degree (p /ₘ q) ≤ Polynomial.degree p

theorem Polynomial.degree_divByMonic_lt {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : Polynomial.Monic q) (hp0 : p ≠ 0) (h0q : 0 < Polynomial.degree q) : Polynomial.degree (p /ₘ q) < Polynomial.degree p

theorem Polynomial.natDegree_divByMonic {R : Type u} [Ring R] (f : Polynomial R) {g : Polynomial R} (hg : Polynomial.Monic g) : Polynomial.natDegree (f /ₘ g) = Polynomial.natDegree f - Polynomial.natDegree g

theorem Polynomial.div_modByMonic_unique {R : Type u} [Ring R] {f : Polynomial R} {g : Polynomial R} (q : Polynomial R) (r : Polynomial R) (hg : Polynomial.Monic g) (h : r + g * q = f ∧ Polynomial.degree r < Polynomial.degree g) : f /ₘ g = q ∧ f %ₘ g = r

theorem Polynomial.map_mod_divByMonic {R : Type u} {S : Type v} [Ring R] {p : Polynomial R} {q : Polynomial R} [Ring S] (f : R →+* S) (hq : Polynomial.Monic q) : 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_divByMonic {R : Type u} {S : Type v} [Ring R] {p : Polynomial R} {q : Polynomial R} [Ring S] (f : R →+* S) (hq : Polynomial.Monic q) : Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q

theorem Polynomial.map_modByMonic {R : Type u} {S : Type v} [Ring R] {p : Polynomial R} {q : Polynomial R} [Ring S] (f : R →+* S) (hq : Polynomial.Monic q) : Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q

theorem Polynomial.dvd_iff_modByMonic_eq_zero {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) : p %ₘ q = 0 ↔ q ∣ p

theorem Polynomial.map_dvd_map {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Injective ⇑f) {x : Polynomial R} {y : Polynomial R} (hx : Polynomial.Monic x) : Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y

@[simp]

theorem Polynomial.modByMonic_one {R : Type u} [Ring R] (p : Polynomial R) : p %ₘ 1 = 0

@[simp]

theorem Polynomial.divByMonic_one {R : Type u} [Ring R] (p : Polynomial R) : p /ₘ 1 = p

theorem Polynomial.sum_modByMonic_coeff {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) {n : ℕ} (hn : Polynomial.degree q ≤ ↑n) : (Finset.sum Finset.univ fun (i : Fin n) => (Polynomial.monomial ↑i) (Polynomial.coeff (p %ₘ q) ↑i)) = p %ₘ q

theorem Polynomial.mul_div_mod_by_monic_cancel_left {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmo : Polynomial.Monic q) : q * p /ₘ q = p

theorem Polynomial.coeff_divByMonic_X_sub_C_rec {R : Type u} [Ring R] (p : Polynomial R) (a : R) (n : ℕ) : Polynomial.coeff (p /ₘ (Polynomial.X - Polynomial.C a)) n = Polynomial.coeff p (n + 1) + a * Polynomial.coeff (p /ₘ (Polynomial.X - Polynomial.C a)) (n + 1)

theorem Polynomial.coeff_divByMonic_X_sub_C {R : Type u} [Ring R] (p : Polynomial R) (a : R) (n : ℕ) : Polynomial.coeff (p /ₘ (Polynomial.X - Polynomial.C a)) n = Finset.sum (Finset.Icc (n + 1) (Polynomial.natDegree p)) fun (i : ℕ) => a ^ (i - (n + 1)) * Polynomial.coeff p i

theorem Polynomial.not_isField (R : Type u) [Ring R] : ¬IsField (Polynomial R)

def Polynomial.decidableDvdMonic {R : Type u} [Ring R] {q : Polynomial R} [DecidableEq R] (p : Polynomial R) (hq : Polynomial.Monic q) : Decidable (q ∣ p)

An algorithm for deciding polynomial divisibility. The algorithm is "compute p %ₘ q and compare to 0". See polynomial.modByMonic for the algorithm that computes %ₘ.

Equations

• Polynomial.decidableDvdMonic p hq = decidable_of_iff (p %ₘ q = 0) (_ : p %ₘ q = 0 ↔ q ∣ p)

theorem Polynomial.multiplicity_X_sub_C_finite {R : Type u} [Ring R] {p : Polynomial R} (a : R) (h0 : p ≠ 0) : multiplicity.Finite (Polynomial.X - Polynomial.C a) p

def Polynomial.rootMultiplicity {R : Type u} [Ring R] (a : R) (p : Polynomial R) : ℕ

The largest power of X - C a which divides p. This could be computable via the divisibility algorithm Polynomial.decidableDvdMonic, as shown by Polynomial.rootMultiplicity_eq_nat_find_of_nonzero which has a computable RHS.

Equations

• Polynomial.rootMultiplicity a p = if h0 : p = 0 then 0 else let x := fun (n : ℕ) => Not.decidable; Nat.find (_ : multiplicity.Finite (Polynomial.X - Polynomial.C a) p)

theorem Polynomial.rootMultiplicity_eq_nat_find_of_nonzero {R : Type u} [Ring R] [DecidableEq R] {p : Polynomial R} (p0 : p ≠ 0) {a : R} : Polynomial.rootMultiplicity a p = Nat.find (_ : multiplicity.Finite (Polynomial.X - Polynomial.C a) p)

theorem Polynomial.rootMultiplicity_eq_multiplicity {R : Type u} [Ring R] [DecidableEq R] [DecidableRel fun (x x_1 : Polynomial R) => x ∣ x_1] (p : Polynomial R) (a : R) : Polynomial.rootMultiplicity a p = if h0 : p = 0 then 0 else (multiplicity (Polynomial.X - Polynomial.C a) p).get (_ : multiplicity.Finite (Polynomial.X - Polynomial.C a) p)

@[simp]

theorem Polynomial.rootMultiplicity_zero {R : Type u} [Ring R] {x : R} : Polynomial.rootMultiplicity x 0 = 0

@[simp]

theorem Polynomial.rootMultiplicity_C {R : Type u} [Ring R] (r : R) (a : R) : Polynomial.rootMultiplicity a (Polynomial.C r) = 0

theorem Polynomial.pow_rootMultiplicity_dvd {R : Type u} [Ring R] (p : Polynomial R) (a : R) : (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p ∣ p

theorem Polynomial.pow_mul_divByMonic_rootMultiplicity_eq {R : Type u} [Ring R] (p : Polynomial R) (a : R) : (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) = p

theorem Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd {R : Type u} [Ring R] (p : Polynomial R) (hp : p ≠ 0) (a : R) : ∃ (q : Polynomial R), p = (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * q ∧ ¬Polynomial.X - Polynomial.C a ∣ q

@[simp]

theorem Polynomial.modByMonic_X_sub_C_eq_C_eval {R : Type u} [CommRing R] (p : Polynomial R) (a : R) : p %ₘ (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)

theorem Polynomial.mul_divByMonic_eq_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} : (Polynomial.X - Polynomial.C a) * (p /ₘ (Polynomial.X - Polynomial.C a)) = p ↔ Polynomial.IsRoot p a

theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} : Polynomial.X - Polynomial.C a ∣ p ↔ Polynomial.IsRoot p a

theorem Polynomial.X_sub_C_dvd_sub_C_eval {R : Type u} {a : R} [CommRing R] {p : Polynomial R} : Polynomial.X - Polynomial.C a ∣ p - Polynomial.C (Polynomial.eval a p)

theorem Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero {R : Type u} {a : R} [CommRing R] {b : Polynomial R} {P : Polynomial (Polynomial R)} : P ∈ Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C a), Polynomial.X - Polynomial.C b} ↔ Polynomial.eval a (Polynomial.eval b P) = 0

theorem Polynomial.modByMonic_X {R : Type u} [CommRing R] (p : Polynomial R) : p %ₘ Polynomial.X = Polynomial.C (Polynomial.eval 0 p)

theorem Polynomial.eval₂_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) {x : S} (hx : Polynomial.eval₂ f x q = 0) : Polynomial.eval₂ f x (p %ₘ q) = Polynomial.eval₂ f x p

theorem Polynomial.sub_dvd_eval_sub {R : Type u} [CommRing R] (a : R) (b : R) (p : Polynomial R) : a - b ∣ Polynomial.eval a p - Polynomial.eval b p

theorem Polynomial.ker_evalRingHom {R : Type u} [CommRing R] (x : R) : RingHom.ker (Polynomial.evalRingHom x) = Ideal.span {Polynomial.X - Polynomial.C x}

@[simp]

theorem Polynomial.rootMultiplicity_eq_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} {x : R} : Polynomial.rootMultiplicity x p = 0 ↔ Polynomial.IsRoot p x → p = 0

theorem Polynomial.rootMultiplicity_eq_zero {R : Type u} [CommRing R] {p : Polynomial R} {x : R} (h : ¬Polynomial.IsRoot p x) : Polynomial.rootMultiplicity x p = 0

@[simp]

theorem Polynomial.rootMultiplicity_pos' {R : Type u} [CommRing R] {p : Polynomial R} {x : R} : 0 < Polynomial.rootMultiplicity x p ↔ p ≠ 0 ∧ Polynomial.IsRoot p x

theorem Polynomial.rootMultiplicity_pos {R : Type u} [CommRing R] {p : Polynomial R} (hp : p ≠ 0) {x : R} : 0 < Polynomial.rootMultiplicity x p ↔ Polynomial.IsRoot p x

theorem Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero {R : Type u} [CommRing R] {p : Polynomial R} (a : R) (hp : p ≠ 0) : Polynomial.eval a (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) ≠ 0