# Theory of univariate polynomials #

We define the multiset of roots of a polynomial, and prove basic results about it.

## Main definitions #

• Polynomial.roots p: The multiset containing all the roots of p, including their multiplicities.
• Polynomial.rootSet p E: The set of distinct roots of p in an algebra E.

## Main statements #

• Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C: If a polynomial has as many roots as its degree, it can be written as the product of its leading coefficient with ∏ (X - a) where a ranges through its roots.
noncomputable def Polynomial.roots {R : Type u} [] [] (p : ) :

roots p noncomputably gives a multiset containing all the roots of p, including their multiplicities.

Equations
• p.roots = if h : p = 0 then else
Instances For
theorem Polynomial.roots_def {R : Type u} [] [] [] (p : ) [Decidable (p = 0)] :
p.roots = if h : p = 0 then else
@[simp]
theorem Polynomial.roots_zero {R : Type u} [] [] :
theorem Polynomial.card_roots {R : Type u} [] [] {p : } (hp0 : p 0) :
(Multiset.card p.roots) p.degree
theorem Polynomial.card_roots' {R : Type u} [] [] (p : ) :
Multiset.card p.roots p.natDegree
theorem Polynomial.card_roots_sub_C {R : Type u} [] [] {p : } {a : R} (hp0 : 0 < p.degree) :
(Multiset.card (p - Polynomial.C a).roots) p.degree
theorem Polynomial.card_roots_sub_C' {R : Type u} [] [] {p : } {a : R} (hp0 : 0 < p.degree) :
Multiset.card (p - Polynomial.C a).roots p.natDegree
@[simp]
theorem Polynomial.count_roots {R : Type u} {a : R} [] [] [] (p : ) :
Multiset.count a p.roots =
@[simp]
theorem Polynomial.mem_roots' {R : Type u} {a : R} [] [] {p : } :
a p.roots p 0 p.IsRoot a
theorem Polynomial.mem_roots {R : Type u} {a : R} [] [] {p : } (hp : p 0) :
a p.roots p.IsRoot a
theorem Polynomial.ne_zero_of_mem_roots {R : Type u} {a : R} [] [] {p : } (h : a p.roots) :
p 0
theorem Polynomial.isRoot_of_mem_roots {R : Type u} {a : R} [] [] {p : } (h : a p.roots) :
p.IsRoot a
theorem Polynomial.mem_roots_iff_aeval_eq_zero {R : Type u} [] [] {p : } {x : R} (w : p 0) :
x p.roots () p = 0
theorem Polynomial.card_le_degree_of_subset_roots {R : Type u} [] [] {p : } {Z : } (h : Z.val p.roots) :
Z.card p.natDegree
theorem Polynomial.finite_setOf_isRoot {R : Type u} [] [] {p : } (hp : p 0) :
{x : R | p.IsRoot x}.Finite
theorem Polynomial.eq_zero_of_infinite_isRoot {R : Type u} [] [] (p : ) (h : {x : R | p.IsRoot x}.Infinite) :
p = 0
theorem Polynomial.exists_max_root {R : Type u} [] [] [] (p : ) (hp : p 0) :
∃ (x₀ : R), ∀ (x : R), p.IsRoot xx x₀
theorem Polynomial.exists_min_root {R : Type u} [] [] [] (p : ) (hp : p 0) :
∃ (x₀ : R), ∀ (x : R), p.IsRoot xx₀ x
theorem Polynomial.eq_of_infinite_eval_eq {R : Type u} [] [] (p : ) (q : ) (h : {x : R | = }.Infinite) :
p = q
theorem Polynomial.roots_mul {R : Type u} [] [] {p : } {q : } (hpq : p * q 0) :
(p * q).roots = p.roots + q.roots
theorem Polynomial.roots.le_of_dvd {R : Type u} [] [] {p : } {q : } (h : q 0) :
p qp.roots q.roots
theorem Polynomial.mem_roots_sub_C' {R : Type u} [] [] {p : } {a : R} {x : R} :
x (p - Polynomial.C a).roots p Polynomial.C a = a
theorem Polynomial.mem_roots_sub_C {R : Type u} [] [] {p : } {a : R} {x : R} (hp0 : 0 < p.degree) :
x (p - Polynomial.C a).roots = a
@[simp]
theorem Polynomial.roots_X_sub_C {R : Type u} [] [] (r : R) :
(Polynomial.X - Polynomial.C r).roots = {r}
@[simp]
theorem Polynomial.roots_X {R : Type u} [] [] :
Polynomial.X.roots = {0}
@[simp]
theorem Polynomial.roots_C {R : Type u} [] [] (x : R) :
(Polynomial.C x).roots = 0
@[simp]
theorem Polynomial.roots_one {R : Type u} [] [] :
@[simp]
theorem Polynomial.roots_C_mul {R : Type u} {a : R} [] [] (p : ) (ha : a 0) :
(Polynomial.C a * p).roots = p.roots
@[simp]
theorem Polynomial.roots_smul_nonzero {R : Type u} {a : R} [] [] (p : ) (ha : a 0) :
(a p).roots = p.roots
@[simp]
theorem Polynomial.roots_neg {R : Type u} [] [] (p : ) :
(-p).roots = p.roots
theorem Polynomial.roots_list_prod {R : Type u} [] [] (L : List ()) :
0LL.prod.roots = (L).bind Polynomial.roots
theorem Polynomial.roots_multiset_prod {R : Type u} [] [] (m : ) :
0mm.prod.roots = m.bind Polynomial.roots
theorem Polynomial.roots_prod {R : Type u} [] [] {ι : Type u_1} (f : ι) (s : ) :
s.prod f 0(s.prod f).roots = s.val.bind fun (i : ι) => (f i).roots
@[simp]
theorem Polynomial.roots_pow {R : Type u} [] [] (p : ) (n : ) :
(p ^ n).roots = n p.roots
theorem Polynomial.roots_X_pow {R : Type u} [] [] (n : ) :
(Polynomial.X ^ n).roots = n {0}
theorem Polynomial.roots_C_mul_X_pow {R : Type u} {a : R} [] [] (ha : a 0) (n : ) :
(Polynomial.C a * Polynomial.X ^ n).roots = n {0}
@[simp]
theorem Polynomial.roots_monomial {R : Type u} {a : R} [] [] (ha : a 0) (n : ) :
( a).roots = n {0}
theorem Polynomial.roots_prod_X_sub_C {R : Type u} [] [] (s : ) :
(as, (Polynomial.X - Polynomial.C a)).roots = s.val
@[simp]
theorem Polynomial.roots_multiset_prod_X_sub_C {R : Type u} [] [] (s : ) :
(Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod.roots = s
theorem Polynomial.card_roots_X_pow_sub_C {R : Type u} [] [] {n : } (hn : 0 < n) (a : R) :
Multiset.card (Polynomial.X ^ n - Polynomial.C a).roots n
def Polynomial.nthRoots {R : Type u} [] [] (n : ) (a : R) :

nthRoots n a noncomputably returns the solutions to x ^ n = a

Equations
• = (Polynomial.X ^ n - Polynomial.C a).roots
Instances For
@[simp]
theorem Polynomial.mem_nthRoots {R : Type u} [] [] {n : } (hn : 0 < n) {a : R} {x : R} :
x x ^ n = a
@[simp]
theorem Polynomial.nthRoots_zero {R : Type u} [] [] (r : R) :
= 0
@[simp]
theorem Polynomial.nthRoots_zero_right {R : Type u_1} [] [] (n : ) :
theorem Polynomial.card_nthRoots {R : Type u} [] [] (n : ) (a : R) :
Multiset.card () n
@[simp]
theorem Polynomial.nthRoots_two_eq_zero_iff {R : Type u} [] [] {r : R} :
= 0
def Polynomial.nthRootsFinset (n : ) (R : Type u_1) [] [] :

The multiset nthRoots ↑n (1 : R) as a Finset.

Equations
• = ().toFinset
Instances For
theorem Polynomial.nthRootsFinset_def (n : ) (R : Type u_1) [] [] [] :
= ().toFinset
@[simp]
theorem Polynomial.mem_nthRootsFinset {R : Type u} [] [] {n : } (h : 0 < n) {x : R} :
x ^ n = 1
@[simp]
theorem Polynomial.nthRootsFinset_zero {R : Type u} [] [] :
theorem Polynomial.mul_mem_nthRootsFinset {R : Type u} {n : } [] [] {η₁ : R} {η₂ : R} (hη₁ : ) (hη₂ : ) :
η₁ * η₂
theorem Polynomial.ne_zero_of_mem_nthRootsFinset {R : Type u} {n : } [] [] {η : R} (hη : ) :
η 0
theorem Polynomial.one_mem_nthRootsFinset {R : Type u} {n : } [] [] (hn : 0 < n) :
theorem Polynomial.zero_of_eval_zero {R : Type u} [] [] [] (p : ) (h : ∀ (x : R), = 0) :
p = 0
theorem Polynomial.funext {R : Type u} [] [] [] {p : } {q : } (ext : ∀ (r : R), = ) :
p = q
@[reducible, inline]
noncomputable abbrev Polynomial.aroots {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] :

Given a polynomial p with coefficients in a ring T and a T-algebra S, aroots p S is the multiset of roots of p regarded as a polynomial over S.

Equations
Instances For
theorem Polynomial.aroots_def {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] :
p.aroots S = (Polynomial.map () p).roots
theorem Polynomial.mem_aroots' {S : Type v} {T : Type w} [] [] [] [Algebra T S] {p : } {a : S} :
a p.aroots S Polynomial.map () p 0 () p = 0
theorem Polynomial.mem_aroots {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {p : } {a : S} :
a p.aroots S p 0 () p = 0
theorem Polynomial.aroots_mul {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {p : } {q : } (hpq : p * q 0) :
(p * q).aroots S = p.aroots S + q.aroots S
@[simp]
theorem Polynomial.aroots_X_sub_C {S : Type v} {T : Type w} [] [] [] [Algebra T S] (r : T) :
(Polynomial.X - Polynomial.C r).aroots S = {() r}
@[simp]
theorem Polynomial.aroots_X {S : Type v} {T : Type w} [] [] [] [Algebra T S] :
Polynomial.X.aroots S = {0}
@[simp]
theorem Polynomial.aroots_C {S : Type v} {T : Type w} [] [] [] [Algebra T S] (a : T) :
(Polynomial.C a).aroots S = 0
@[simp]
theorem Polynomial.aroots_zero {T : Type w} [] (S : Type u_1) [] [] [Algebra T S] :
= 0
@[simp]
theorem Polynomial.aroots_one {S : Type v} {T : Type w} [] [] [] [Algebra T S] :
= 0
@[simp]
theorem Polynomial.aroots_neg {S : Type v} {T : Type w} [] [] [] [Algebra T S] (p : ) :
(-p).aroots S = p.aroots S
@[simp]
theorem Polynomial.aroots_C_mul {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {a : T} (p : ) (ha : a 0) :
(Polynomial.C a * p).aroots S = p.aroots S
@[simp]
theorem Polynomial.aroots_smul_nonzero {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {a : T} (p : ) (ha : a 0) :
(a p).aroots S = p.aroots S
@[simp]
theorem Polynomial.aroots_pow {S : Type v} {T : Type w} [] [] [] [Algebra T S] (p : ) (n : ) :
(p ^ n).aroots S = n p.aroots S
theorem Polynomial.aroots_X_pow {S : Type v} {T : Type w} [] [] [] [Algebra T S] (n : ) :
(Polynomial.X ^ n).aroots S = n {0}
theorem Polynomial.aroots_C_mul_X_pow {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {a : T} (ha : a 0) (n : ) :
(Polynomial.C a * Polynomial.X ^ n).aroots S = n {0}
@[simp]
theorem Polynomial.aroots_monomial {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {a : T} (ha : a 0) (n : ) :
( a).aroots S = n {0}
def Polynomial.rootSet {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] :
Set S

The set of distinct roots of p in S.

If you have a non-separable polynomial, use Polynomial.aroots for the multiset where multiple roots have the appropriate multiplicity.

Equations
• p.rootSet S = (p.aroots S).toFinset
Instances For
theorem Polynomial.rootSet_def {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] [] :
p.rootSet S = (p.aroots S).toFinset
@[simp]
theorem Polynomial.rootSet_C {S : Type v} {T : Type w} [] [] [] [Algebra T S] (a : T) :
(Polynomial.C a).rootSet S =
@[simp]
theorem Polynomial.rootSet_zero {T : Type w} [] (S : Type u_1) [] [] [Algebra T S] :
@[simp]
theorem Polynomial.rootSet_one {T : Type w} [] (S : Type u_1) [] [] [Algebra T S] :
@[simp]
theorem Polynomial.rootSet_neg {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] :
(-p).rootSet S = p.rootSet S
instance Polynomial.rootSetFintype {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] :
Fintype (p.rootSet S)
Equations
theorem Polynomial.rootSet_finite {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] :
(p.rootSet S).Finite
theorem Polynomial.bUnion_roots_finite {R : Type u_1} {S : Type u_2} [] [] [] [] (m : R →+* S) (d : ) {U : Set R} (h : U.Finite) :
(⋃ (f : ), ⋃ (_ : f.natDegree d ∀ (i : ), f.coeff i U), ().roots.toFinset).Finite

The set of roots of all polynomials of bounded degree and having coefficients in a finite set is finite.

theorem Polynomial.mem_rootSet' {T : Type w} [] {p : } {S : Type u_1} [] [] [Algebra T S] {a : S} :
a p.rootSet S Polynomial.map () p 0 () p = 0
theorem Polynomial.mem_rootSet {T : Type w} [] {p : } {S : Type u_1} [] [] [Algebra T S] [] {a : S} :
a p.rootSet S p 0 () p = 0
theorem Polynomial.mem_rootSet_of_ne {T : Type w} [] {p : } {S : Type u_1} [] [] [Algebra T S] [] (hp : p 0) {a : S} :
a p.rootSet S () p = 0
theorem Polynomial.rootSet_maps_to' {T : Type w} [] {p : } {S : Type u_1} {S' : Type u_2} [] [] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S'] (hp : Polynomial.map (algebraMap T S') p = 0Polynomial.map () p = 0) (f : S →ₐ[T] S') :
Set.MapsTo (f) (p.rootSet S) (p.rootSet S')
theorem Polynomial.ne_zero_of_mem_rootSet {S : Type v} {T : Type w} [] {p : } [] [] [Algebra T S] {a : S} (h : a p.rootSet S) :
p 0
theorem Polynomial.aeval_eq_zero_of_mem_rootSet {S : Type v} {T : Type w} [] {p : } [] [] [Algebra T S] {a : S} (hx : a p.rootSet S) :
() p = 0
theorem Polynomial.rootSet_mapsTo {T : Type w} [] {p : } {S : Type u_1} {S' : Type u_2} [] [] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S'] [] (f : S →ₐ[T] S') :
Set.MapsTo (f) (p.rootSet S) (p.rootSet S')
theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R : Type u_1} [] [] (p : ) {ι : Type u_2} [] {f : ιR} (hf : ) (heval : ∀ (i : ι), Polynomial.eval (f i) p = 0) (hcard : p.natDegree < ) :
p = 0
theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' {R : Type u_1} [] [] (p : ) (s : ) (heval : is, = 0) (hcard : p.natDegree < s.card) :
p = 0
theorem Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_card {R : Type u} [] [] (f : ) (hf : ∀ (r : R), = 0) (hfR : f.natDegree < ) :
f = 0
theorem Polynomial.exists_eval_ne_zero_of_natDegree_lt_card {R : Type u} [] [] (f : ) (hf : f 0) (hfR : f.natDegree < ) :
∃ (r : R), 0
theorem Polynomial.monic_prod_multiset_X_sub_C {R : Type u} [] [] {p : } :
(Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod.Monic
theorem Polynomial.prod_multiset_root_eq_finset_root {R : Type u} [] [] {p : } [] :
(Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod = ap.roots.toFinset, (Polynomial.X - Polynomial.C a) ^
theorem Polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [] [] (p : ) :
(Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod p

The product ∏ (X - a) for a inside the multiset p.roots divides p.

theorem Multiset.prod_X_sub_C_dvd_iff_le_roots {R : Type u} [] [] {p : } (hp : p 0) (s : ) :
(Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod p s p.roots

A Galois connection.

theorem Polynomial.exists_prod_multiset_X_sub_C_mul {R : Type u} [] [] (p : ) :
∃ (q : ), (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod * q = p Multiset.card p.roots + q.natDegree = p.natDegree q.roots = 0
theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C {R : Type u} [] [] {p : } (hroots : Multiset.card p.roots = p.natDegree) :
Polynomial.C p.leadingCoeff * (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod = p

A polynomial p that has as many roots as its degree can be written p = p.leadingCoeff * ∏(X - a), for a in p.roots.

theorem Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq {R : Type u} [] [] {p : } (hp : p.Monic) (hroots : Multiset.card p.roots = p.natDegree) :
(Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod = p

A monic polynomial p that has as many roots as its degree can be written p = ∏(X - a), for a in p.roots.

theorem Polynomial.Monic.isUnit_leadingCoeff_of_dvd {R : Type u} [] [] {a : } {p : } (hp : p.Monic) (hap : a p) :
theorem Polynomial.Monic.irreducible_iff_degree_lt {R : Type u} [] [] {p : } (p_monic : p.Monic) (p_1 : p 1) :
∀ (q : ), q.degree (p.natDegree / 2)q p

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

See also: Polynomial.Monic.irreducible_iff_natDegree.

theorem Polynomial.le_rootMultiplicity_map {A : Type u_1} {B : Type u_2} [] [] {p : } {f : A →+* B} (hmap : 0) (a : A) :
theorem Polynomial.eq_rootMultiplicity_map {A : Type u_1} {B : Type u_2} [] [] {p : } {f : A →+* B} (hf : ) (a : A) :
theorem Polynomial.count_map_roots {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (hmap : 0) (b : B) :
Multiset.count b (Multiset.map (f) p.roots)
theorem Polynomial.count_map_roots_of_injective {A : Type u_1} {B : Type u_2} [] [] [] [] (p : ) {f : A →+* B} (hf : ) (b : B) :
Multiset.count b (Multiset.map (f) p.roots)
theorem Polynomial.map_roots_le {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (h : 0) :
Multiset.map (f) p.roots ().roots
theorem Polynomial.map_roots_le_of_injective {A : Type u_1} {B : Type u_2} [] [] [] [] (p : ) {f : A →+* B} (hf : ) :
Multiset.map (f) p.roots ().roots
theorem Polynomial.card_roots_le_map {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (h : 0) :
Multiset.card p.roots Multiset.card ().roots
theorem Polynomial.card_roots_le_map_of_injective {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (hf : ) :
Multiset.card p.roots Multiset.card ().roots
theorem Polynomial.roots_map_of_injective_of_card_eq_natDegree {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (hf : ) (hroots : Multiset.card p.roots = p.natDegree) :
Multiset.map (f) p.roots = ().roots