# 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`.

source
theorem Polynomial.X_dvd_iff {R : Type u} [Semiring R] {f : Polynomial R} :
X ∣ f ↔ f.coeff 0 = 0
source
theorem Polynomial.X_pow_dvd_iff {R : Type u} [Semiring R] {f : Polynomial R} {n : ℕ} :
X ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0
source
theorem Polynomial.finiteMultiplicity_of_degree_pos_of_monic {R : Type u} [Semiring R] {p q : Polynomial R} (hp : 0 < p.degree) (hmp : p.Monic) (hq : q ≠ 0) :
FiniteMultiplicity p q
source
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 * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
source
@[irreducible]
noncomputable def Polynomial.divModByMonicAux {R : Type u} [Ring R] (_p : Polynomial R) {q : Polynomial R} :
q.Monic → Polynomial R × Polynomial R

See `divByMonic`.

Equations

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

Instances For

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

`divByMonic`, denoted as `p /ₘ q`, gives the quotient of `p` by a monic polynomial `q`.

Equations

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

Instances For

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

`modByMonic`, denoted as `p %ₘ q`, gives the remainder of `p` by a monic polynomial `q`.

Equations

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

Instances For

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

`divByMonic`, denoted as `p /ₘ q`, 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))

Instances For

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

`modByMonic`, denoted as `p %ₘ q`, 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))

Instances For

source
@[irreducible]
theorem Polynomial.degree_modByMonic_lt {R : Type u} [Ring R] [Nontrivial R] (p : Polynomial R) {q : Polynomial R} (_hq : q.Monic) :
(p %ₘ q).degree < q.degree
source
theorem Polynomial.natDegree_modByMonic_lt {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmq : q.Monic) (hq : q ≠ 1) :
(p %ₘ q).natDegree < q.natDegree
source
@[simp]
theorem Polynomial.zero_modByMonic {R : Type u} [Ring R] (p : Polynomial R) :
0 %ₘ p = 0
source
@[simp]
theorem Polynomial.zero_divByMonic {R : Type u} [Ring R] (p : Polynomial R) :
0 /ₘ p = 0
source
@[simp]
theorem Polynomial.modByMonic_zero {R : Type u} [Ring R] (p : Polynomial R) :
p %ₘ 0 = p
source
@[simp]
theorem Polynomial.divByMonic_zero {R : Type u} [Ring R] (p : Polynomial R) :
p /ₘ 0 = 0
source
theorem Polynomial.divByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬q.Monic) :
p /ₘ q = 0
source
theorem Polynomial.modByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬q.Monic) :
p %ₘ q = p
source
theorem Polynomial.modByMonic_eq_self_iff {R : Type u} [Ring R] {p q : Polynomial R} [Nontrivial R] (hq : q.Monic) :
p %ₘ q = p ↔ p.degree < q.degree
source
theorem Polynomial.degree_modByMonic_le {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : q.Monic) :
(p %ₘ q).degree ≤ q.degree
source
theorem Polynomial.degree_modByMonic_le_left {R : Type u} [Ring R] {p q : Polynomial R} :
(p %ₘ q).degree ≤ p.degree
source
theorem Polynomial.natDegree_modByMonic_le {R : Type u} [Ring R] (p : Polynomial R) {g : Polynomial R} (hg : g.Monic) :
(p %ₘ g).natDegree ≤ g.natDegree
source
theorem Polynomial.natDegree_modByMonic_le_left {R : Type u} [Ring R] {p q : Polynomial R} :
(p %ₘ q).natDegree ≤ p.natDegree
source
theorem Polynomial.X_dvd_sub_C {R : Type u} [Ring R] {p : Polynomial R} :
X ∣ p - C (p.coeff 0)
source
@[irreducible]
theorem Polynomial.modByMonic_eq_sub_mul_div {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (_hq : q.Monic) :
p %ₘ q = p - q * (p /ₘ q)
source
theorem Polynomial.modByMonic_add_div {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : q.Monic) :
p %ₘ q + q * (p /ₘ q) = p
source
theorem Polynomial.divByMonic_eq_zero_iff {R : Type u} [Ring R] {p q : Polynomial R} [Nontrivial R] (hq : q.Monic) :
p /ₘ q = 0 ↔ p.degree < q.degree
source
theorem Polynomial.degree_add_divByMonic {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) (h : q.degree ≤ p.degree) :
q.degree + (p /ₘ q).degree = p.degree
source
theorem Polynomial.degree_divByMonic_le {R : Type u} [Ring R] (p q : Polynomial R) :
(p /ₘ q).degree ≤ p.degree
source
theorem Polynomial.degree_divByMonic_lt {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : q.Monic) (hp0 : p ≠ 0) (h0q : 0 < q.degree) :
(p /ₘ q).degree < p.degree
source
theorem Polynomial.natDegree_divByMonic {R : Type u} [Ring R] (f : Polynomial R) {g : Polynomial R} (hg : g.Monic) :
(f /ₘ g).natDegree = f.natDegree - g.natDegree
source
theorem Polynomial.div_modByMonic_unique {R : Type u} [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
source
theorem Polynomial.map_mod_divByMonic {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) :
map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
source
theorem Polynomial.map_divByMonic {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) :
map f (p /ₘ q) = map f p /ₘ map f q
source
theorem Polynomial.map_modByMonic {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) :
map f (p %ₘ q) = map f p %ₘ map f q
source
theorem Polynomial.modByMonic_eq_zero_iff_dvd {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) :
p %ₘ q = 0 ↔ q ∣ p
source
@[simp]
theorem Polynomial.self_mul_modByMonic {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) :
q * p %ₘ q = 0

See `Polynomial.mul_self_modByMonic` for the other multiplication order. That version, unlike this one, requires commutativity.

source
theorem Polynomial.map_dvd_map {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Injective ⇑f) {x y : Polynomial R} (hx : x.Monic) :
map f x ∣ map f y ↔ x ∣ y
source
@[simp]
theorem Polynomial.modByMonic_one {R : Type u} [Ring R] (p : Polynomial R) :
p %ₘ 1 = 0
source
@[simp]
theorem Polynomial.divByMonic_one {R : Type u} [Ring R] (p : Polynomial R) :
p /ₘ 1 = p
source
theorem Polynomial.sum_modByMonic_coeff {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) {n : ℕ} (hn : q.degree ≤ ↑n) :
∑ i : Fin n, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q
source
theorem Polynomial.mul_divByMonic_cancel_left {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmo : q.Monic) :
q * p /ₘ q = p
source
theorem Polynomial.coeff_divByMonic_X_sub_C_rec {R : Type u} [Ring R] (p : Polynomial R) (a : R) (n : ℕ) :
(p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)
source
theorem Polynomial.coeff_divByMonic_X_sub_C {R : Type u} [Ring R] (p : Polynomial R) (a : R) (n : ℕ) :
(p /ₘ (X - C a)).coeff n = ∑ i ∈ Finset.Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
source
theorem Polynomial.not_isField (R : Type u) [Ring R] :
¬IsField (Polynomial R)
source
def Polynomial.decidableDvdMonic {R : Type u} [Ring R] {q : Polynomial R} [DecidableEq R] (p : Polynomial R) (hq : q.Monic) :
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) ⋯

Instances For

source
theorem Polynomial.finiteMultiplicity_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} (a : R) (h0 : p ≠ 0) :
FiniteMultiplicity (X - C a) p
source
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

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

Instances For

source
theorem Polynomial.rootMultiplicity_eq_nat_find_of_nonzero {R : Type u} [Ring R] [DecidableEq R] {p : Polynomial R} (p0 : p ≠ 0) {a : R} :
rootMultiplicity a p = Nat.find ⋯
source
theorem Polynomial.rootMultiplicity_eq_multiplicity {R : Type u} [Ring R] [DecidableEq R] (p : Polynomial R) (a : R) :
rootMultiplicity a p = if p = 0 then 0 else multiplicity (X - C a) p
source
@[simp]
theorem Polynomial.rootMultiplicity_zero {R : Type u} [Ring R] {x : R} :
rootMultiplicity x 0 = 0
source
@[simp]
theorem Polynomial.rootMultiplicity_C {R : Type u} [Ring R] (r a : R) :
rootMultiplicity a (C r) = 0
source
theorem Polynomial.pow_rootMultiplicity_dvd {R : Type u} [Ring R] (p : Polynomial R) (a : R) :
(X - C a) ^ rootMultiplicity a p ∣ p
source
theorem Polynomial.pow_mul_divByMonic_rootMultiplicity_eq {R : Type u} [Ring R] (p : Polynomial R) (a : R) :
(X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
source
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 = (X - C a) ^ rootMultiplicity a p * q ∧ ¬X - C a ∣ q
source
@[simp]
theorem Polynomial.modByMonic_X_sub_C_eq_C_eval {R : Type u} [CommRing R] (p : Polynomial R) (a : R) :
p %ₘ (X - C a) = C (eval a p)
source
theorem Polynomial.mul_divByMonic_eq_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
(X - C a) * (p /ₘ (X - C a)) = p ↔ p.IsRoot a
source
theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
X - C a ∣ p ↔ p.IsRoot a
source
theorem Polynomial.X_sub_C_dvd_sub_C_eval {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
X - C a ∣ p - C (eval a p)
source
theorem Polynomial.modByMonic_X {R : Type u} [CommRing R] (p : Polynomial R) :
p %ₘ X = C (eval 0 p)
source
theorem Polynomial.eval₂_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} {p q : Polynomial R} (hq : q.Monic) {x : S} (hx : eval₂ f x q = 0) :
eval₂ f x (p %ₘ q) = eval₂ f x p
source
theorem Polynomial.sub_dvd_eval_sub {R : Type u} [CommRing R] (a b : R) (p : Polynomial R) :
a - b ∣ eval a p - eval b p
source
@[simp]
theorem Polynomial.rootMultiplicity_eq_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} {x : R} :
rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0
source
theorem Polynomial.rootMultiplicity_eq_zero {R : Type u} [CommRing R] {p : Polynomial R} {x : R} (h : ¬p.IsRoot x) :
rootMultiplicity x p = 0
source
@[simp]
theorem Polynomial.rootMultiplicity_pos' {R : Type u} [CommRing R] {p : Polynomial R} {x : R} :
0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
source
theorem Polynomial.rootMultiplicity_pos {R : Type u} [CommRing R] {p : Polynomial R} (hp : p ≠ 0) {x : R} :
0 < rootMultiplicity x p ↔ p.IsRoot x
source
theorem Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero {R : Type u} [CommRing R] {p : Polynomial R} (a : R) (hp : p ≠ 0) :
eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0
source
@[simp]
theorem Polynomial.mul_self_modByMonic {R : Type u} [CommRing R] {p q : Polynomial R} (hq : q.Monic) :
p * q %ₘ q = 0

See `Polynomial.self_mul_modByMonic` for the other multiplication order. This version, unlike that one, requires commutativity.

source
theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [CommRing R] {p₁ p₂ q : Polynomial R} (hq : q.Monic) (h : q ∣ p₁ - p₂) :
p₁ %ₘ q = p₂ %ₘ q
source
theorem Polynomial.add_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (p₁ p₂ : Polynomial R) :
(p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
source
theorem Polynomial.neg_modByMonic {R : Type u} [CommRing R] (p q : Polynomial R) :
-p %ₘ q = -(p %ₘ q)
source
theorem Polynomial.sub_modByMonic {R : Type u} [CommRing R] (p₁ p₂ q : Polynomial R) :
(p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q
source
theorem Polynomial.eval_divByMonic_eq_trailingCoeff_comp {R : Type u} [CommRing R] {p : Polynomial R} {t : R} :
eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff
source
theorem Polynomial.le_rootMultiplicity_iff {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p ≠ 0) {a : R} {n : ℕ} :
n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p

The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff `(X - a) ^ n` divides `p`.

source
theorem Polynomial.rootMultiplicity_le_iff {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p ≠ 0) (a : R) (n : ℕ) :
rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p
source
theorem Polynomial.rootMultiplicity_add {R : Type u} [CommRing R] {p q : Polynomial R} (a : R) (hzero : p + q ≠ 0) :
min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)

The multiplicity of `p + q` is at least the minimum of the multiplicities.

source
theorem Polynomial.le_rootMultiplicity_mul {R : Type u} [CommRing R] {p q : Polynomial R} (x : R) (hpq : p * q ≠ 0) :
rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)
source
theorem Polynomial.rootMultiplicity_le_rootMultiplicity_of_dvd {R : Type u} [CommRing R] {p q : Polynomial R} (hq : q ≠ 0) (hpq : p ∣ q) (x : R) :
rootMultiplicity x p ≤ rootMultiplicity x q
source
theorem Polynomial.pow_rootMultiplicity_not_dvd {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p ≠ 0) (a : R) :
¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p
source
theorem Polynomial.rootMultiplicity_eq_natTrailingDegree' {R : Type u} [CommRing R] {p : Polynomial R} :
rootMultiplicity 0 p = p.natTrailingDegree

See `Polynomial.rootMultiplicity_eq_natTrailingDegree` for the general case.

source
theorem Polynomial.leadingCoeff_divByMonic_of_monic {R : Type u} [CommRing R] {p q : Polynomial R} (hmonic : q.Monic) (hdegree : q.degree ≤ p.degree) :
(p /ₘ q).leadingCoeff = p.leadingCoeff

Division by a monic polynomial doesn't change the leading coefficient.

source
theorem Polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) {x : R} (hx : p.IsRoot x) :
p.degree = 1
source
theorem Irreducible.not_isRoot_of_natDegree_ne_one {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) {x : R} :
¬p.IsRoot x
source
theorem Irreducible.isRoot_eq_bot_of_natDegree_ne_one {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) :
p.IsRoot = ⊥
source
theorem Irreducible.subsingleton_isRoot {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] [IsLeftCancelMulZero R] (hi : Irreducible p) :
{x : R | p.IsRoot x}.Subsingleton
source
theorem Polynomial.leadingCoeff_divByMonic_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (hp : p.degree ≠ 0) (a : R) :
(p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff
source
theorem Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (hpq : p ∣ q) (h₁ : q.natDegree ≤ p.natDegree) (h₂ : p.leadingCoeff = q.leadingCoeff) :
p = q
source
theorem Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (hpq : p ∣ q) (h₁ : q.natDegree ≤ p.natDegree) (h₂ : q.leadingCoeff ∣ p.leadingCoeff) :
Associated p q
source
theorem Polynomial.associated_of_dvd_of_natDegree_le {K : Type u_1} [Field K] {p q : Polynomial K} (hpq : p ∣ q) (hq : q ≠ 0) (h₁ : q.natDegree ≤ p.natDegree) :
Associated p q
source
theorem Polynomial.associated_of_dvd_of_degree_eq {K : Type u_1} [Field K] {p q : Polynomial K} (hpq : p ∣ q) (h₁ : p.degree = q.degree) :
Associated p q
source
theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.Monic) (hdiv : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) :
q = C q.leadingCoeff * p
source
theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (hdiv : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) :
q = p