# Theory of univariate polynomials #

We prove basic results about univariate polynomials.

theorem Polynomial.natDegree_pos_of_aeval_root {R : Type u} {S : Type v} [] [] [Algebra R S] {p : } (hp : p 0) {z : S} (hz : () p = 0) (inj : ∀ (x : R), () x = 0x = 0) :
0 < p.natDegree
theorem Polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [] [] [Algebra R S] {p : } (hp : p 0) {z : S} (hz : () p = 0) (inj : ∀ (x : R), () x = 0x = 0) :
0 < p.degree
theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [] {q : } (hq : q.Monic) {p₁ : } {p₂ : } (h : q p₁ - p₂) :
p₁.modByMonic q = p₂.modByMonic q
theorem Polynomial.add_modByMonic {R : Type u} [] {q : } (p₁ : ) (p₂ : ) :
(p₁ + p₂).modByMonic q = p₁.modByMonic q + p₂.modByMonic q
theorem Polynomial.smul_modByMonic {R : Type u} [] {q : } (c : R) (p : ) :
(c p).modByMonic q = c p.modByMonic q
@[simp]
theorem Polynomial.modByMonicHom_apply {R : Type u} [] (q : ) (p : ) :
q.modByMonicHom p = p.modByMonic q
def Polynomial.modByMonicHom {R : Type u} [] (q : ) :

_ %ₘ q as an R-linear map.

Equations
• q.modByMonicHom = { toFun := fun (p : ) => p.modByMonic q, map_add' := , map_smul' := }
Instances For
theorem Polynomial.neg_modByMonic {R : Type u} [] (p : ) (mod : ) :
(-p).modByMonic mod = -p.modByMonic mod
theorem Polynomial.sub_modByMonic {R : Type u} [] (a : ) (b : ) (mod : ) :
(a - b).modByMonic mod = a.modByMonic mod - b.modByMonic mod
theorem Polynomial.aeval_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [] [Ring S] [Algebra R S] {p : } {q : } (hq : q.Monic) {x : S} (hx : () q = 0) :
() (p.modByMonic q) = () p
instance Polynomial.instNoZeroDivisors {R : Type u} [] [] :
Equations
• =
theorem Polynomial.natDegree_mul {R : Type u} [] [] {p : } {q : } (hp : p 0) (hq : q 0) :
(p * q).natDegree = p.natDegree + q.natDegree
theorem Polynomial.trailingDegree_mul {R : Type u} [] [] {p : } {q : } :
(p * q).trailingDegree = p.trailingDegree + q.trailingDegree
@[simp]
theorem Polynomial.natDegree_pow {R : Type u} [] [] (p : ) (n : ) :
(p ^ n).natDegree = n * p.natDegree
theorem Polynomial.degree_le_mul_left {R : Type u} [] [] {q : } (p : ) (hq : q 0) :
p.degree (p * q).degree
theorem Polynomial.natDegree_le_of_dvd {R : Type u} [] [] {p : } {q : } (h1 : p q) (h2 : q 0) :
p.natDegree q.natDegree
theorem Polynomial.degree_le_of_dvd {R : Type u} [] [] {p : } {q : } (h1 : p q) (h2 : q 0) :
p.degree q.degree
theorem Polynomial.eq_zero_of_dvd_of_degree_lt {R : Type u} [] [] {p : } {q : } (h₁ : p q) (h₂ : q.degree < p.degree) :
q = 0
theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt {R : Type u} [] [] {p : } {q : } (h₁ : p q) (h₂ : q.natDegree < p.natDegree) :
q = 0
theorem Polynomial.not_dvd_of_degree_lt {R : Type u} [] [] {p : } {q : } (h0 : q 0) (hl : q.degree < p.degree) :
¬p q
theorem Polynomial.not_dvd_of_natDegree_lt {R : Type u} [] [] {p : } {q : } (h0 : q 0) (hl : q.natDegree < p.natDegree) :
¬p q
theorem Polynomial.natDegree_sub_eq_of_prod_eq {R : Type u} [] [] {p₁ : } {p₂ : } {q₁ : } {q₂ : } (hp₁ : p₁ 0) (hq₁ : q₁ 0) (hp₂ : p₂ 0) (hq₂ : q₂ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :
p₁.natDegree - q₁.natDegree = p₂.natDegree - q₂.natDegree

This lemma is useful for working with the intDegree of a rational function.

theorem Polynomial.natDegree_eq_zero_of_isUnit {R : Type u} [] [] {p : } (h : ) :
p.natDegree = 0
theorem Polynomial.degree_eq_zero_of_isUnit {R : Type u} [] [] {p : } [] (h : ) :
p.degree = 0
@[simp]
theorem Polynomial.degree_coe_units {R : Type u} [] [] [] (u : ()ˣ) :
(u).degree = 0
theorem Polynomial.isUnit_iff {R : Type u} [] [] {p : } :
∃ (r : R), Polynomial.C r = p

Characterization of a unit of a polynomial ring over an integral domain R. See Polynomial.isUnit_iff_coeff_isUnit_isNilpotent when R is a commutative ring.

theorem Polynomial.not_isUnit_of_degree_pos {R : Type u} [] [] (p : ) (hpl : 0 < p.degree) :
theorem Polynomial.not_isUnit_of_natDegree_pos {R : Type u} [] [] (p : ) (hpl : 0 < p.natDegree) :
theorem Polynomial.irreducible_of_monic {R : Type u} [] [] {p : } (hp : p.Monic) (hp1 : p 1) :
∀ (f g : ), f.Monicg.Monicf * g = pf = 1 g = 1
theorem Polynomial.Monic.irreducible_iff_natDegree {R : Type u} [] [] {p : } (hp : p.Monic) :
p 1 ∀ (f g : ), f.Monicg.Monicf * g = pf.natDegree = 0 g.natDegree = 0
theorem Polynomial.Monic.irreducible_iff_natDegree' {R : Type u} [] [] {p : } (hp : p.Monic) :
p 1 ∀ (f g : ), f.Monicg.Monicf * g = pg.natDegreeFinset.Ioc 0 (p.natDegree / 2)
theorem Polynomial.Monic.irreducible_iff_lt_natDegree_lt {R : Type u} [] [] {p : } (hp : p.Monic) (hp1 : p 1) :
∀ (q : ), q.Monicq.natDegree Finset.Ioc 0 (p.natDegree / 2)¬q p

Alternate phrasing of Polynomial.Monic.irreducible_iff_natDegree' where we only have to check one divisor at a time.

theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff {R : Type u} [] [] {p : } (hm : p.Monic) (hnd : p.natDegree = 2) :
∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ p.coeff 1 = c₁ + c₂
theorem Polynomial.root_mul {R : Type u} {a : R} [] [] {p : } {q : } :
(p * q).IsRoot a p.IsRoot a q.IsRoot a
theorem Polynomial.root_or_root_of_root_mul {R : Type u} {a : R} [] [] {p : } {q : } (h : (p * q).IsRoot a) :
p.IsRoot a q.IsRoot a
instance Polynomial.instIsDomain {R : Type u} [Ring R] [] :
Equations
• =
theorem Polynomial.Monic.C_dvd_iff_isUnit {R : Type u} [] {p : } (hp : p.Monic) {a : R} :
Polynomial.C a p
theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [] {a : } {p : } (ha : ¬) (hap : a p) (hp : p.Monic) :
0 < a.degree
theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [] {a : } {p : } (ha : ¬) (hap : a p) (hp : p.Monic) :
0 < a.natDegree
theorem Polynomial.degree_pos_of_monic_of_not_isUnit {R : Type u} [] {a : } (hu : ¬) (ha : a.Monic) :
0 < a.degree
theorem Polynomial.natDegree_pos_of_monic_of_not_isUnit {R : Type u} [] {a : } (hu : ¬) (ha : a.Monic) :
0 < a.natDegree
theorem Polynomial.le_rootMultiplicity_iff {R : Type u} [] {p : } (p0 : p 0) {a : R} {n : } :
(Polynomial.X - Polynomial.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.

theorem Polynomial.rootMultiplicity_le_iff {R : Type u} [] {p : } (p0 : p 0) (a : R) (n : ) :
¬(Polynomial.X - Polynomial.C a) ^ (n + 1) p
theorem Polynomial.pow_rootMultiplicity_not_dvd {R : Type u} [] {p : } (p0 : p 0) (a : R) :
¬(Polynomial.X - Polynomial.C a) ^ () p
theorem Polynomial.X_sub_C_pow_dvd_iff {R : Type u} [] {p : } {t : R} {n : } :
(Polynomial.X - Polynomial.C t) ^ n p Polynomial.X ^ n p.comp (Polynomial.X + Polynomial.C t)
theorem Polynomial.comp_X_add_C_eq_zero_iff {R : Type u} [] {p : } (t : R) :
p.comp (Polynomial.X + Polynomial.C t) = 0 p = 0
theorem Polynomial.comp_X_add_C_ne_zero_iff {R : Type u} [] {p : } (t : R) :
p.comp (Polynomial.X + Polynomial.C t) 0 p 0
theorem Polynomial.rootMultiplicity_eq_rootMultiplicity {R : Type u} [] {p : } {t : R} :
= Polynomial.rootMultiplicity 0 (p.comp (Polynomial.X + Polynomial.C t))
theorem Polynomial.rootMultiplicity_eq_natTrailingDegree' {R : Type u} [] {p : } :
= p.natTrailingDegree
theorem Polynomial.rootMultiplicity_eq_natTrailingDegree {R : Type u} [] {p : } {t : R} :
= (p.comp (Polynomial.X + Polynomial.C t)).natTrailingDegree
theorem Polynomial.eval_divByMonic_eq_trailingCoeff_comp {R : Type u} [] {p : } {t : R} :
Polynomial.eval t (p.divByMonic ((Polynomial.X - Polynomial.C t) ^ )) = (p.comp (Polynomial.X + Polynomial.C t)).trailingCoeff
theorem Polynomial.Monic.mem_nonZeroDivisors {R : Type u} [] {p : } (h : p.Monic) :
theorem Polynomial.mem_nonZeroDivisors_of_leadingCoeff {R : Type u} [] {p : } (h : p.leadingCoeff ) :
theorem Polynomial.rootMultiplicity_mul_X_sub_C_pow {R : Type u} [] {p : } {a : R} {n : } (h : p 0) :
Polynomial.rootMultiplicity a (p * (Polynomial.X - Polynomial.C a) ^ n) =
theorem Polynomial.rootMultiplicity_X_sub_C_pow {R : Type u} [] [] (a : R) (n : ) :
Polynomial.rootMultiplicity a ((Polynomial.X - Polynomial.C a) ^ n) = n

The multiplicity of a as root of (X - a) ^ n is n.

theorem Polynomial.rootMultiplicity_X_sub_C_self {R : Type u} [] [] {x : R} :
Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C x) = 1
theorem Polynomial.rootMultiplicity_X_sub_C {R : Type u} [] [] [] {x : R} {y : R} :
Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C y) = if x = y then 1 else 0
theorem Polynomial.rootMultiplicity_add {R : Type u} [] {p : } {q : } (a : R) (hzero : p + q 0) :

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

theorem Polynomial.le_rootMultiplicity_mul {R : Type u} [] {p : } {q : } (x : R) (hpq : p * q 0) :
theorem Polynomial.rootMultiplicity_mul' {R : Type u} [] {p : } {q : } {x : R} (hpq : Polynomial.eval x (p.divByMonic ((Polynomial.X - Polynomial.C x) ^ )) * Polynomial.eval x (q.divByMonic ((Polynomial.X - Polynomial.C x) ^ )) 0) :
@[simp]
theorem Polynomial.natDegree_coe_units {R : Type u} [] [] (u : ()ˣ) :
(u).natDegree = 0
theorem Polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [] [] (u : ()ˣ) :
(u).coeff 0 0
theorem Polynomial.degree_eq_degree_of_associated {R : Type u} [] [] {p : } {q : } (h : ) :
p.degree = q.degree
theorem Polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [] [] {p : } (hi : ) {x : R} (hx : p.IsRoot x) :
p.degree = 1
theorem Polynomial.leadingCoeff_divByMonic_of_monic {R : Type u} [] {p : } {q : } (hmonic : q.Monic) (hdegree : q.degree p.degree) :

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

theorem Polynomial.leadingCoeff_divByMonic_X_sub_C {R : Type u} [] [] (p : ) (hp : p.degree 0) (a : R) :
theorem Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [] [] {p : } {q : } (hpq : p q) (h₁ : q.natDegree p.natDegree) (h₂ : p.leadingCoeff = q.leadingCoeff) :
p = q
theorem Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [] [] {p : } {q : } (hpq : p q) (h₁ : q.natDegree p.natDegree) (h₂ : q.leadingCoeff p.leadingCoeff) :
theorem Polynomial.associated_of_dvd_of_natDegree_le {K : Type u_1} [] {p : } {q : } (hpq : p q) (hq : q 0) (h₁ : q.natDegree p.natDegree) :
theorem Polynomial.associated_of_dvd_of_degree_eq {K : Type u_1} [] {p : } {q : } (hpq : p q) (h₁ : p.degree = q.degree) :
theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [] {p : } {q : } (hp : p.Monic) (hdiv : p q) (hdeg : q.natDegree p.natDegree) :
q = Polynomial.C q.leadingCoeff * p
theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [] {p : } {q : } (hp : p.Monic) (hq : q.Monic) (hdiv : p q) (hdeg : q.natDegree p.natDegree) :
q = p
theorem Polynomial.prime_X_sub_C {R : Type u} [] [] (r : R) :
Prime (Polynomial.X - Polynomial.C r)
theorem Polynomial.prime_X {R : Type u} [] [] :
Prime Polynomial.X
theorem Polynomial.Monic.prime_of_degree_eq_one {R : Type u} [] [] {p : } (hp1 : p.degree = 1) (hm : p.Monic) :
theorem Polynomial.irreducible_X_sub_C {R : Type u} [] [] (r : R) :
Irreducible (Polynomial.X - Polynomial.C r)
theorem Polynomial.irreducible_X {R : Type u} [] [] :
Irreducible Polynomial.X
theorem Polynomial.Monic.irreducible_of_degree_eq_one {R : Type u} [] [] {p : } (hp1 : p.degree = 1) (hm : p.Monic) :
@[simp]
theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card {R : Type u} [] [] (s : ) :
(Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod.natDegree = Multiset.card s
theorem Polynomial.Monic.comp {R : Type u} [] [] {p : } {q : } (hp : p.Monic) (hq : q.Monic) (h : q.natDegree 0) :
(p.comp q).Monic
theorem Polynomial.Monic.comp_X_add_C {R : Type u} [] [] {p : } (hp : p.Monic) (r : R) :
(p.comp (Polynomial.X + Polynomial.C r)).Monic
theorem Polynomial.Monic.comp_X_sub_C {R : Type u} [] [] {p : } (hp : p.Monic) (r : R) :
(p.comp (Polynomial.X - Polynomial.C r)).Monic
theorem Polynomial.units_coeff_zero_smul {R : Type u} [] [] (c : ()ˣ) (p : ) :
(c).coeff 0 p = c * p
theorem Polynomial.comp_eq_zero_iff {R : Type u} [] [] {p : } {q : } :
p.comp q = 0 p = 0 Polynomial.eval (q.coeff 0) p = 0 q = Polynomial.C (q.coeff 0)
theorem Polynomial.isCoprime_X_sub_C_of_isUnit_sub {R : Type u_1} [] {a : R} {b : R} (h : IsUnit (a - b)) :
IsCoprime (Polynomial.X - Polynomial.C a) (Polynomial.X - Polynomial.C b)
theorem Polynomial.pairwise_coprime_X_sub_C {K : Type u_1} [] {I : Type v} {s : IK} (H : ) :
Pairwise (IsCoprime on fun (i : I) => Polynomial.X - Polynomial.C (s i))
theorem Polynomial.rootMultiplicity_mul {R : Type u} [] [] {p : } {q : } {x : R} (hpq : p * q 0) :
theorem Polynomial.exists_multiset_roots {R : Type u} [] [] [] {p : } :
p 0∃ (s : ), (Multiset.card s) p.degree ∀ (a : R),
theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map {R : Type u} {S : Type v} [] [] [] (φ : R →+* S) {f : } (hf : IsUnit f.leadingCoeff) (H : IsUnit ()) :
theorem Polynomial.Monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [] [] [] [] (φ : R →+* S) (f : ) (h_mon : f.Monic) (h_irr : ) :

A polynomial over an integral domain R is irreducible if it is monic and irreducible after mapping into an integral domain S.

A special case of this lemma is that a polynomial over ℤ is irreducible if it is monic and irreducible over ℤ/pℤ for some prime p.