# 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} [] {f : } :
Polynomial.X f = 0
theorem Polynomial.X_pow_dvd_iff {R : Type u} [] {f : } {n : } :
Polynomial.X ^ n f d < n, = 0
theorem Polynomial.multiplicity_finite_of_degree_pos_of_monic {R : Type u} [] {p : } {q : } (hp : ) (hmp : ) (hq : q 0) :
theorem Polynomial.div_wf_lemma {R : Type u} [Ring R] {p : } {q : } (h : p 0) (hq : ) :
Polynomial.degree (p - q * (Polynomial.C * Polynomial.X ^ )) <
noncomputable def Polynomial.divModByMonicAux {R : Type u} [Ring R] (_p : ) {q : } :

See divByMonic.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Polynomial.divByMonic {R : Type u} [Ring R] (p : ) (q : ) :

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

Equations
• p /ₘ q = if hq : then ().1 else 0
Instances For
def Polynomial.modByMonic {R : Type u} [Ring R] (p : ) (q : ) :

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

Equations
• p %ₘ q = if hq : then ().2 else p
Instances For

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

Equations
Instances For

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

Equations
Instances For
theorem Polynomial.degree_modByMonic_lt {R : Type u} [Ring R] [] (p : ) {q : } (_hq : ) :
theorem Polynomial.natDegree_modByMonic_lt {R : Type u} [Ring R] (p : ) {q : } (hmq : ) (hq : q 1) :
@[simp]
theorem Polynomial.zero_modByMonic {R : Type u} [Ring R] (p : ) :
0 %ₘ p = 0
@[simp]
theorem Polynomial.zero_divByMonic {R : Type u} [Ring R] (p : ) :
0 /ₘ p = 0
@[simp]
theorem Polynomial.modByMonic_zero {R : Type u} [Ring R] (p : ) :
p %ₘ 0 = p
@[simp]
theorem Polynomial.divByMonic_zero {R : Type u} [Ring R] (p : ) :
p /ₘ 0 = 0
theorem Polynomial.divByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : } (p : ) (hq : ) :
p /ₘ q = 0
theorem Polynomial.modByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : } (p : ) (hq : ) :
p %ₘ q = p
theorem Polynomial.modByMonic_eq_self_iff {R : Type u} [Ring R] {p : } {q : } [] (hq : ) :
p %ₘ q = p
theorem Polynomial.degree_modByMonic_le {R : Type u} [Ring R] (p : ) {q : } (hq : ) :
theorem Polynomial.natDegree_modByMonic_le {R : Type u} [Ring R] (p : ) {g : } (hg : ) :
theorem Polynomial.X_dvd_sub_C {R : Type u} [Ring R] {p : } :
Polynomial.X p - Polynomial.C ()
theorem Polynomial.modByMonic_eq_sub_mul_div {R : Type u} [Ring R] (p : ) {q : } (_hq : ) :
p %ₘ q = p - q * (p /ₘ q)
theorem Polynomial.modByMonic_add_div {R : Type u} [Ring R] (p : ) {q : } (hq : ) :
p %ₘ q + q * (p /ₘ q) = p
theorem Polynomial.divByMonic_eq_zero_iff {R : Type u} [Ring R] {p : } {q : } [] (hq : ) :
p /ₘ q = 0
theorem Polynomial.degree_add_divByMonic {R : Type u} [Ring R] {p : } {q : } (hq : ) (h : ) :
theorem Polynomial.degree_divByMonic_le {R : Type u} [Ring R] (p : ) (q : ) :
theorem Polynomial.degree_divByMonic_lt {R : Type u} [Ring R] (p : ) {q : } (hq : ) (hp0 : p 0) (h0q : ) :
theorem Polynomial.natDegree_divByMonic {R : Type u} [Ring R] (f : ) {g : } (hg : ) :
theorem Polynomial.div_modByMonic_unique {R : Type u} [Ring R] {f : } {g : } (q : ) (r : ) (hg : ) (h : r + g * q = f ) :
f /ₘ g = q f %ₘ g = r
theorem Polynomial.map_mod_divByMonic {R : Type u} {S : Type v} [Ring R] {p : } {q : } [Ring S] (f : R →+* S) (hq : ) :
theorem Polynomial.map_divByMonic {R : Type u} {S : Type v} [Ring R] {p : } {q : } [Ring S] (f : R →+* S) (hq : ) :
theorem Polynomial.map_modByMonic {R : Type u} {S : Type v} [Ring R] {p : } {q : } [Ring S] (f : R →+* S) (hq : ) :
theorem Polynomial.dvd_iff_modByMonic_eq_zero {R : Type u} [Ring R] {p : } {q : } (hq : ) :
p %ₘ q = 0 q p
theorem Polynomial.map_dvd_map {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (hf : ) {x : } {y : } (hx : ) :
x y
@[simp]
theorem Polynomial.modByMonic_one {R : Type u} [Ring R] (p : ) :
p %ₘ 1 = 0
@[simp]
theorem Polynomial.divByMonic_one {R : Type u} [Ring R] (p : ) :
p /ₘ 1 = p
theorem Polynomial.sum_modByMonic_coeff {R : Type u} [Ring R] {p : } {q : } (hq : ) {n : } (hn : ) :
(Finset.sum Finset.univ fun (i : Fin n) => () (Polynomial.coeff (p %ₘ q) i)) = p %ₘ q
theorem Polynomial.mul_div_mod_by_monic_cancel_left {R : Type u} [Ring R] (p : ) {q : } (hmo : ) :
q * p /ₘ q = p
theorem Polynomial.coeff_divByMonic_X_sub_C_rec {R : Type u} [Ring R] (p : ) (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 : ) (a : R) (n : ) :
Polynomial.coeff (p /ₘ (Polynomial.X - Polynomial.C a)) n = Finset.sum (Finset.Icc (n + 1) ) fun (i : ) => a ^ (i - (n + 1)) *
def Polynomial.decidableDvdMonic {R : Type u} [Ring R] {q : } [] (p : ) (hq : ) :

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
Instances For
theorem Polynomial.multiplicity_X_sub_C_finite {R : Type u} [Ring R] {p : } (a : R) (h0 : p 0) :
multiplicity.Finite (Polynomial.X - Polynomial.C a) p
def Polynomial.rootMultiplicity {R : Type u} [Ring R] (a : R) (p : ) :

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
Instances For
theorem Polynomial.rootMultiplicity_eq_nat_find_of_nonzero {R : Type u} [Ring R] [] {p : } (p0 : p 0) {a : R} :
= Nat.find (_ : multiplicity.Finite (Polynomial.X - Polynomial.C a) p)
theorem Polynomial.rootMultiplicity_eq_multiplicity {R : Type u} [Ring R] [] [DecidableRel fun (x x_1 : ) => x x_1] (p : ) (a : R) :
= 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} :
@[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 : ) (a : R) :
(Polynomial.X - Polynomial.C a) ^ p
theorem Polynomial.pow_mul_divByMonic_rootMultiplicity_eq {R : Type u} [Ring R] (p : ) (a : R) :
(Polynomial.X - Polynomial.C a) ^ * (p /ₘ (Polynomial.X - Polynomial.C a) ^ ) = p
theorem Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd {R : Type u} [Ring R] (p : ) (hp : p 0) (a : R) :
∃ (q : ), p = (Polynomial.X - Polynomial.C a) ^ * q ¬Polynomial.X - Polynomial.C a q
@[simp]
theorem Polynomial.modByMonic_X_sub_C_eq_C_eval {R : Type u} [] (p : ) (a : R) :
p %ₘ (Polynomial.X - Polynomial.C a) = Polynomial.C ()
theorem Polynomial.mul_divByMonic_eq_iff_isRoot {R : Type u} {a : R} [] {p : } :
(Polynomial.X - Polynomial.C a) * (p /ₘ (Polynomial.X - Polynomial.C a)) = p
theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [] {p : } :
Polynomial.X - Polynomial.C a p
theorem Polynomial.X_sub_C_dvd_sub_C_eval {R : Type u} {a : R} [] {p : } :
Polynomial.X - Polynomial.C a p - Polynomial.C ()
theorem Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero {R : Type u} {a : R} [] {b : } {P : } :
P Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C a), Polynomial.X - Polynomial.C b} = 0
theorem Polynomial.modByMonic_X {R : Type u} [] (p : ) :
p %ₘ Polynomial.X = Polynomial.C ()
theorem Polynomial.eval₂_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [] [] {f : R →+* S} {p : } {q : } (hq : ) {x : S} (hx : = 0) :
theorem Polynomial.sub_dvd_eval_sub {R : Type u} [] (a : R) (b : R) (p : ) :
a - b -
theorem Polynomial.ker_evalRingHom {R : Type u} [] (x : R) :
= Ideal.span {Polynomial.X - Polynomial.C x}
@[simp]
theorem Polynomial.rootMultiplicity_eq_zero_iff {R : Type u} [] {p : } {x : R} :
p = 0
theorem Polynomial.rootMultiplicity_eq_zero {R : Type u} [] {p : } {x : R} (h : ) :
@[simp]
theorem Polynomial.rootMultiplicity_pos' {R : Type u} [] {p : } {x : R} :
p 0
theorem Polynomial.rootMultiplicity_pos {R : Type u} [] {p : } (hp : p 0) {x : R} :
theorem Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero {R : Type u} [] {p : } (a : R) (hp : p 0) :
Polynomial.eval a (p /ₘ (Polynomial.X - Polynomial.C a) ^ ) 0