# Theory of univariate polynomials #

This file starts looking like the ring theory of $R[X]$

theorem Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero {R : Type u} [] (p : ) (t : R) (hnezero : Polynomial.derivative p 0) :
Polynomial.rootMultiplicity t (Polynomial.derivative p)
theorem Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors {R : Type u} [] {p : } {t : R} (hpt : p.IsRoot t) (hnzd : ) :
Polynomial.rootMultiplicity t (Polynomial.derivative p) =
theorem Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity {R : Type u} [] {p : } {t : R} {n : } (hn : ) :
((Polynomial.derivative)^[n] p).IsRoot t
theorem Polynomial.eval_iterate_derivative_rootMultiplicity {R : Type u} [] {p : } {t : R} :
Polynomial.eval t ((Polynomial.derivative)^[] p) = .factorial Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ )
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors {R : Type u} [] {p : } {t : R} {n : } (h : p 0) (hroot : mn, ((Polynomial.derivative)^[m] p).IsRoot t) (hnzd : n.factorial ) :
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' {R : Type u} [] {p : } {t : R} {n : } (h : p 0) (hroot : mn, ((Polynomial.derivative)^[m] p).IsRoot t) (hnzd : mn, m 0m ) :
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors {R : Type u} [] {p : } {t : R} {n : } (h : p 0) (hnzd : n.factorial ) :
mn, ((Polynomial.derivative)^[m] p).IsRoot t
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' {R : Type u} [] {p : } {t : R} {n : } (h : p 0) (hnzd : mn, m 0m ) :
mn, ((Polynomial.derivative)^[m] p).IsRoot t
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative {R : Type u} [] {p : } {t : R} (h : p 0) :
m1, ((Polynomial.derivative)^[m] p).IsRoot t
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot {R : Type u} [] {p : } {t : R} (h : p 0) :
p.IsRoot t (Polynomial.derivative p).IsRoot t
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd {R : Type u} [] [] [] {p : } {t : R} (h : p 0) :
(gcd p (Polynomial.derivative p)).IsRoot t
theorem Polynomial.derivative_rootMultiplicity_of_root {R : Type u} [] [] [] {p : } {t : R} (hpt : p.IsRoot t) :
Polynomial.rootMultiplicity t (Polynomial.derivative p) =
theorem Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity {R : Type u} [] [] [] (p : ) (t : R) :
Polynomial.rootMultiplicity t (Polynomial.derivative p)
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative {R : Type u} [] [] [] {p : } {t : R} {n : } (h : p 0) (hroot : mn, ((Polynomial.derivative)^[m] p).IsRoot t) :
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative {R : Type u} [] [] [] {p : } {t : R} {n : } (h : p 0) :
mn, ((Polynomial.derivative)^[m] p).IsRoot t
instance Polynomial.instNormalizationMonoid {R : Type u} [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Polynomial.coe_normUnit {R : Type u} [] [] {p : } :
theorem Polynomial.leadingCoeff_normalize {R : Type u} [] [] (p : ) :
theorem Polynomial.Monic.normalize_eq_self {R : Type u} [] [] {p : } (hp : p.Monic) :
normalize p = p
theorem Polynomial.roots_normalize {R : Type u} [] [] {p : } :
(normalize p).roots = p.roots
theorem Polynomial.normUnit_X {R : Type u} [] [] :
normUnit Polynomial.X = 1
theorem Polynomial.X_eq_normalize {R : Type u} [] [] :
Polynomial.X = normalize Polynomial.X
theorem Polynomial.degree_pos_of_ne_zero_of_nonunit {R : Type u} [] {p : } (hp0 : p 0) (hp : ¬) :
0 < p.degree
@[simp]
theorem Polynomial.map_eq_zero {R : Type u} {S : Type v} [] {p : } [] [] (f : R →+* S) :
= 0 p = 0
theorem Polynomial.map_ne_zero {R : Type u} {S : Type v} [] {p : } [] [] {f : R →+* S} (hp : p 0) :
0
@[simp]
theorem Polynomial.degree_map {R : Type u} {S : Type v} [] [] [] (p : ) (f : R →+* S) :
().degree = p.degree
@[simp]
theorem Polynomial.natDegree_map {R : Type u} {S : Type v} [] {p : } [] [] (f : R →+* S) :
().natDegree = p.natDegree
@[simp]
theorem Polynomial.leadingCoeff_map {R : Type u} {S : Type v} [] {p : } [] [] (f : R →+* S) :
theorem Polynomial.monic_map_iff {R : Type u} {S : Type v} [] [] [] {f : R →+* S} {p : } :
().Monic p.Monic
theorem Polynomial.isUnit_iff_degree_eq_zero {R : Type u} [] {p : } :
p.degree = 0
def Polynomial.div {R : Type u} [] (p : ) (q : ) :

Division of polynomials. See Polynomial.divByMonic for more details.

Equations
• p.div q = Polynomial.C q.leadingCoeff⁻¹ * (p /ₘ (q * Polynomial.C q.leadingCoeff⁻¹))
Instances For
def Polynomial.mod {R : Type u} [] (p : ) (q : ) :

Remainder of polynomial division. See Polynomial.modByMonic for more details.

Equations
• p.mod q = p %ₘ (q * Polynomial.C q.leadingCoeff⁻¹)
Instances For
instance Polynomial.instDiv {R : Type u} [] :
Div ()
Equations
• Polynomial.instDiv = { div := Polynomial.div }
instance Polynomial.instMod {R : Type u} [] :
Mod ()
Equations
• Polynomial.instMod = { mod := Polynomial.mod }
theorem Polynomial.div_def {R : Type u} [] {p : } {q : } :
p / q = Polynomial.C q.leadingCoeff⁻¹ * (p /ₘ (q * Polynomial.C q.leadingCoeff⁻¹))
theorem Polynomial.mod_def {R : Type u} [] {p : } {q : } :
p % q = p %ₘ (q * Polynomial.C q.leadingCoeff⁻¹)
theorem Polynomial.modByMonic_eq_mod {R : Type u} [] {q : } (p : ) (hq : q.Monic) :
p %ₘ q = p % q
theorem Polynomial.divByMonic_eq_div {R : Type u} [] {q : } (p : ) (hq : q.Monic) :
p /ₘ q = p / q
theorem Polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [] (p : ) (a : R) :
p % (Polynomial.X - Polynomial.C a) = Polynomial.C ()
theorem Polynomial.mul_div_eq_iff_isRoot {R : Type u} {a : R} [] {p : } :
(Polynomial.X - Polynomial.C a) * (p / (Polynomial.X - Polynomial.C a)) = p p.IsRoot a
instance Polynomial.instEuclideanDomain {R : Type u} [] :
Equations
• One or more equations did not get rendered due to their size.
theorem Polynomial.mod_eq_self_iff {R : Type u} [] {p : } {q : } (hq0 : q 0) :
p % q = p p.degree < q.degree
theorem Polynomial.div_eq_zero_iff {R : Type u} [] {p : } {q : } (hq0 : q 0) :
p / q = 0 p.degree < q.degree
theorem Polynomial.degree_add_div {R : Type u} [] {p : } {q : } (hq0 : q 0) (hpq : q.degree p.degree) :
q.degree + (p / q).degree = p.degree
theorem Polynomial.degree_div_le {R : Type u} [] (p : ) (q : ) :
(p / q).degree p.degree
theorem Polynomial.degree_div_lt {R : Type u} [] {p : } {q : } (hp : p 0) (hq : 0 < q.degree) :
(p / q).degree < p.degree
theorem Polynomial.isUnit_map {R : Type u} {k : Type y} [] {p : } [] (f : R →+* k) :
theorem Polynomial.map_div {R : Type u} {k : Type y} [] {p : } {q : } [] (f : R →+* k) :
Polynomial.map f (p / q) = /
theorem Polynomial.map_mod {R : Type u} {k : Type y} [] {p : } {q : } [] (f : R →+* k) :
Polynomial.map f (p % q) = %
theorem Polynomial.gcd_map {R : Type u} {k : Type y} [] {p : } {q : } [] [] [] (f : R →+* k) :
theorem Polynomial.eval₂_gcd_eq_zero {R : Type u} {k : Type y} [] [] [] {ϕ : R →+* k} {f : } {g : } {α : k} (hf : = 0) (hg : = 0) :
= 0
theorem Polynomial.eval_gcd_eq_zero {R : Type u} [] [] {f : } {g : } {α : R} (hf : = 0) (hg : = 0) :
= 0
theorem Polynomial.root_left_of_root_gcd {R : Type u} {k : Type y} [] [] [] {ϕ : R →+* k} {f : } {g : } {α : k} (hα : = 0) :
= 0
theorem Polynomial.root_right_of_root_gcd {R : Type u} {k : Type y} [] [] [] {ϕ : R →+* k} {f : } {g : } {α : k} (hα : = 0) :
= 0
theorem Polynomial.root_gcd_iff_root_left_right {R : Type u} {k : Type y} [] [] [] {ϕ : R →+* k} {f : } {g : } {α : k} :
= 0 = 0 = 0
theorem Polynomial.isRoot_gcd_iff_isRoot_left_right {R : Type u} [] [] {f : } {g : } {α : R} :
().IsRoot α f.IsRoot α g.IsRoot α
theorem Polynomial.isCoprime_map {R : Type u} {k : Type y} [] {p : } {q : } [] (f : R →+* k) :
IsCoprime () ()
theorem Polynomial.mem_roots_map {R : Type u} {k : Type y} [] {p : } [] [] {f : R →+* k} {x : k} (hp : p 0) :
x ().roots = 0
theorem Polynomial.rootSet_monomial {R : Type u} {S : Type v} [] [] [] [Algebra R S] {n : } (hn : n 0) {a : R} (ha : a 0) :
( a).rootSet S = {0}
theorem Polynomial.rootSet_C_mul_X_pow {R : Type u} {S : Type v} [] [] [] [Algebra R S] {n : } (hn : n 0) {a : R} (ha : a 0) :
(Polynomial.C a * Polynomial.X ^ n).rootSet S = {0}
theorem Polynomial.rootSet_X_pow {R : Type u} {S : Type v} [] [] [] [Algebra R S] {n : } (hn : n 0) :
(Polynomial.X ^ n).rootSet S = {0}
theorem Polynomial.rootSet_prod {R : Type u} {S : Type v} [] [] [] [Algebra R S] {ι : Type u_1} (f : ι) (s : ) (h : s.prod f 0) :
(s.prod f).rootSet S = is, (f i).rootSet S
theorem Polynomial.exists_root_of_degree_eq_one {R : Type u} [] {p : } (h : p.degree = 1) :
∃ (x : R), p.IsRoot x
theorem Polynomial.coeff_inv_units {R : Type u} [] (u : ()ˣ) (n : ) :
((u).coeff n)⁻¹ = (u⁻¹).coeff n
theorem Polynomial.monic_normalize {R : Type u} [] {p : } [] (hp0 : p 0) :
(normalize p).Monic
theorem Polynomial.leadingCoeff_div {R : Type u} [] {p : } {q : } (hpq : q.degree p.degree) :
theorem Polynomial.div_C_mul {R : Type u} {a : R} [] {p : } {q : } :
p / (Polynomial.C a * q) = Polynomial.C a⁻¹ * (p / q)
theorem Polynomial.C_mul_dvd {R : Type u} {a : R} [] {p : } {q : } (ha : a 0) :
Polynomial.C a * p q p q
theorem Polynomial.dvd_C_mul {R : Type u} {a : R} [] {p : } {q : } (ha : a 0) :
p Polynomial.C a * q p q
theorem Polynomial.coe_normUnit_of_ne_zero {R : Type u} [] {p : } [] (hp : p 0) :
theorem Polynomial.normalize_monic {R : Type u} [] {p : } [] (h : p.Monic) :
normalize p = p
theorem Polynomial.map_dvd_map' {R : Type u} {k : Type y} [] [] (f : R →+* k) {x : } {y : } :
x y
theorem Polynomial.degree_normalize {R : Type u} [] {p : } [] :
(normalize p).degree = p.degree
theorem Polynomial.prime_of_degree_eq_one {R : Type u} [] {p : } (hp1 : p.degree = 1) :
theorem Polynomial.irreducible_of_degree_eq_one {R : Type u} [] {p : } (hp1 : p.degree = 1) :
theorem Polynomial.not_irreducible_C {R : Type u} [] (x : R) :
¬Irreducible (Polynomial.C x)
theorem Polynomial.degree_pos_of_irreducible {R : Type u} [] {p : } (hp : ) :
0 < p.degree
theorem Polynomial.X_sub_C_mul_divByMonic_eq_sub_modByMonic {K : Type u_1} [] (f : ) (a : K) :
(Polynomial.X - Polynomial.C a) * (f /ₘ (Polynomial.X - Polynomial.C a)) = f - f %ₘ (Polynomial.X - Polynomial.C a)
theorem Polynomial.divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative {K : Type u_1} [] (f : ) (a : K) :
f /ₘ (Polynomial.X - Polynomial.C a) + (Polynomial.X - Polynomial.C a) * Polynomial.derivative (f /ₘ (Polynomial.X - Polynomial.C a)) = Polynomial.derivative f
theorem Polynomial.X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic {K : Type u_1} [] (f : ) {a : K} (hf : Polynomial.X - Polynomial.C a f /ₘ (Polynomial.X - Polynomial.C a)) :
Polynomial.X - Polynomial.C a Polynomial.derivative f
theorem Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type u_1} [] (f : ) (a : K) (hf' : Polynomial.eval a (Polynomial.derivative f) 0) :
IsCoprime (Polynomial.X - Polynomial.C a) (f /ₘ (Polynomial.X - Polynomial.C a))

If f is a polynomial over a field, and a : K satisfies f' a ≠ 0, then f / (X - a) is coprime with X - a. Note that we do not assume f a = 0, because f / (X - a) = (f - f a) / (X - a).

theorem Polynomial.irreducible_iff_degree_lt {R : Type u} [] (p : ) (hp0 : p 0) (hpu : ¬) :
∀ (q : ), q.degree (p.natDegree / 2)q p

To check a polynomial over a field is irreducible, it suffices to check only for divisors that have smaller degree.

See also: Polynomial.Monic.irreducible_iff_natDegree.

theorem Polynomial.irreducible_iff_lt_natDegree_lt {R : Type u} [] {p : } (hp0 : p 0) (hpu : ¬) :
∀ (q : ), q.Monicq.natDegree Finset.Ioc 0 (p.natDegree / 2)¬q p

To check a polynomial p over a field is irreducible, it suffices to check there are no divisors of degree 0 < d ≤ degree p / 2.

See also: Polynomial.Monic.irreducible_iff_natDegree'.

theorem Irreducible.natDegree_pos {F : Type u_1} [] {f : } (h : ) :
0 < f.natDegree

An irreducible polynomial over a field must have positive degree.