# Documentation

Mathlib.Data.Polynomial.RingDivision

# Theory of univariate polynomials #

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

## 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.
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) :
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) :
theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [] {q : } (hq : ) {p₁ : } {p₂ : } (h : q p₁ - p₂) :
p₁ %ₘ q = p₂ %ₘ q
theorem Polynomial.add_modByMonic {R : Type u} [] {q : } (p₁ : ) (p₂ : ) :
(p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
theorem Polynomial.smul_modByMonic {R : Type u} [] {q : } (c : R) (p : ) :
c p %ₘ q = c (p %ₘ q)
@[simp]
theorem Polynomial.modByMonicHom_apply {R : Type u} [] (q : ) (p : ) :
↑() p = p %ₘ q
def Polynomial.modByMonicHom {R : Type u} [] (q : ) :

_ %ₘ q as an R-linear map.

Instances For
theorem Polynomial.aeval_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [] [Ring S] [Algebra R S] {p : } {q : } (hq : ) {x : S} (hx : ↑() q = 0) :
↑() (p %ₘ q) = ↑() p
theorem Polynomial.natDegree_mul {R : Type u} [] [] {p : } {q : } (hp : p 0) (hq : q 0) :
theorem Polynomial.trailingDegree_mul {R : Type u} [] [] {p : } {q : } :
@[simp]
theorem Polynomial.natDegree_pow {R : Type u} [] [] (p : ) (n : ) :
theorem Polynomial.degree_le_mul_left {R : Type u} [] [] {q : } (p : ) (hq : q 0) :
theorem Polynomial.natDegree_le_of_dvd {R : Type u} [] [] {p : } {q : } (h1 : p q) (h2 : q 0) :
theorem Polynomial.degree_le_of_dvd {R : Type u} [] [] {p : } {q : } (h1 : p q) (h2 : q 0) :
theorem Polynomial.eq_zero_of_dvd_of_degree_lt {R : Type u} [] [] {p : } {q : } (h₁ : p q) (h₂ : ) :
q = 0
theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt {R : Type u} [] [] {p : } {q : } (h₁ : p q) (h₂ : ) :
q = 0
theorem Polynomial.not_dvd_of_degree_lt {R : Type u} [] [] {p : } {q : } (h0 : q 0) (hl : ) :
¬p q
theorem Polynomial.not_dvd_of_natDegree_lt {R : Type u} [] [] {p : } {q : } (h0 : q 0) (hl : ) :
¬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₁) :
↑() - ↑() = ↑() - ↑()

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 : ) :
theorem Polynomial.degree_eq_zero_of_isUnit {R : Type u} [] [] {p : } [] (h : ) :
@[simp]
theorem Polynomial.degree_coe_units {R : Type u} [] [] [] (u : ()ˣ) :
theorem Polynomial.isUnit_iff {R : Type u} [] [] {p : } :
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.irreducible_of_monic {R : Type u} [] [] {p : } (hp : ) (hp1 : p 1) :
∀ (f g : ), f * g = pf = 1 g = 1
theorem Polynomial.Monic.irreducible_iff_natDegree {R : Type u} [] [] {p : } (hp : ) :
p 1 ∀ (f g : ), f * g = p
theorem Polynomial.Monic.irreducible_iff_natDegree' {R : Type u} [] [] {p : } (hp : ) :
p 1 ∀ (f g : ), f * g = p¬
theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff {R : Type u} [] [] {p : } (hm : ) (hnd : ) :
c₁ c₂, = c₁ * c₂ = c₁ + c₂
theorem Polynomial.root_mul {R : Type u} {a : R} [] [] {p : } {q : } :
theorem Polynomial.root_or_root_of_root_mul {R : Type u} {a : R} [] [] {p : } {q : } (h : Polynomial.IsRoot (p * q) a) :
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.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.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 : ) (hm : ) :
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 : ) (hm : ) :
theorem Polynomial.eq_of_monic_of_associated {R : Type u} [] [] {p : } {q : } (hp : ) (hq : ) (hpq : ) :
p = q
theorem Polynomial.rootMultiplicity_mul {R : Type u} [] [] {p : } {q : } {x : R} (hpq : p * q 0) :
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_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.exists_multiset_roots {R : Type u} [] [] [] {p : } :
p 0s, ↑(Multiset.card s) ∀ (a : R),
noncomputable def Polynomial.roots {R : Type u} [] [] (p : ) :

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

Instances For
theorem Polynomial.roots_def {R : Type u} [] [] [] (p : ) [Decidable (p = 0)] :
= if h : p = 0 then else Classical.choose (_ : s, ↑(Multiset.card s) ∀ (a : R), )
@[simp]
theorem Polynomial.roots_zero {R : Type u} [] [] :
theorem Polynomial.card_roots {R : Type u} [] [] {p : } (hp0 : p 0) :
↑(Multiset.card ())
theorem Polynomial.card_roots' {R : Type u} [] [] (p : ) :
Multiset.card ()
theorem Polynomial.card_roots_sub_C {R : Type u} [] [] {p : } {a : R} (hp0 : ) :
↑(Multiset.card (Polynomial.roots (p - Polynomial.C a)))
theorem Polynomial.card_roots_sub_C' {R : Type u} [] [] {p : } {a : R} (hp0 : ) :
Multiset.card (Polynomial.roots (p - Polynomial.C a))
@[simp]
theorem Polynomial.count_roots {R : Type u} {a : R} [] [] [] (p : ) :
@[simp]
theorem Polynomial.mem_roots' {R : Type u} {a : R} [] [] {p : } :
p 0
theorem Polynomial.mem_roots {R : Type u} {a : R} [] [] {p : } (hp : p 0) :
theorem Polynomial.ne_zero_of_mem_roots {R : Type u} {a : R} [] [] {p : } (h : ) :
p 0
theorem Polynomial.isRoot_of_mem_roots {R : Type u} {a : R} [] [] {p : } (h : ) :
theorem Polynomial.mem_roots_iff_aeval_eq_zero {R : Type u} [] [] {p : } {x : R} (w : p 0) :
↑() p = 0
theorem Polynomial.card_le_degree_of_subset_roots {R : Type u} [] [] {p : } {Z : } (h : Z.val ) :
theorem Polynomial.finite_setOf_isRoot {R : Type u} [] [] {p : } (hp : p 0) :
Set.Finite {x | }
theorem Polynomial.eq_zero_of_infinite_isRoot {R : Type u} [] [] (p : ) (h : Set.Infinite {x | }) :
p = 0
theorem Polynomial.exists_max_root {R : Type u} [] [] [] (p : ) (hp : p 0) :
x₀, ∀ (x : R), x x₀
theorem Polynomial.exists_min_root {R : Type u} [] [] [] (p : ) (hp : p 0) :
x₀, ∀ (x : R), x₀ x
theorem Polynomial.eq_of_infinite_eval_eq {R : Type u} [] [] (p : ) (q : ) (h : Set.Infinite {x | = }) :
p = q
theorem Polynomial.roots_mul {R : Type u} [] [] {p : } {q : } (hpq : p * q 0) :
theorem Polynomial.roots.le_of_dvd {R : Type u} [] [] {p : } {q : } (h : q 0) :
p q
theorem Polynomial.mem_roots_sub_C' {R : Type u} [] [] {p : } {a : R} {x : R} :
x Polynomial.roots (p - Polynomial.C a) p Polynomial.C a = a
theorem Polynomial.mem_roots_sub_C {R : Type u} [] [] {p : } {a : R} {x : R} (hp0 : ) :
x Polynomial.roots (p - Polynomial.C a) = a
@[simp]
theorem Polynomial.roots_X_sub_C {R : Type u} [] [] (r : R) :
Polynomial.roots (Polynomial.X - Polynomial.C r) = {r}
@[simp]
theorem Polynomial.roots_X {R : Type u} [] [] :
Polynomial.roots Polynomial.X = {0}
@[simp]
theorem Polynomial.roots_C {R : Type u} [] [] (x : R) :
Polynomial.roots (Polynomial.C x) = 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.roots (Polynomial.C a * p) =
@[simp]
theorem Polynomial.roots_smul_nonzero {R : Type u} {a : R} [] [] (p : ) (ha : a 0) :
theorem Polynomial.roots_list_prod {R : Type u} [] [] (L : List ()) :
¬0 L = Multiset.bind (L) Polynomial.roots
theorem Polynomial.roots_multiset_prod {R : Type u} [] [] (m : ) :
¬0 m = Multiset.bind m Polynomial.roots
theorem Polynomial.roots_prod {R : Type u} [] [] {ι : Type u_1} (f : ι) (s : ) :
0 = Multiset.bind s.val fun i => Polynomial.roots (f i)
@[simp]
theorem Polynomial.roots_pow {R : Type u} [] [] (p : ) (n : ) :
theorem Polynomial.roots_X_pow {R : Type u} [] [] (n : ) :
Polynomial.roots (Polynomial.X ^ n) = n {0}
theorem Polynomial.roots_C_mul_X_pow {R : Type u} {a : R} [] [] (ha : a 0) (n : ) :
Polynomial.roots (Polynomial.C a * Polynomial.X ^ n) = n {0}
@[simp]
theorem Polynomial.roots_monomial {R : Type u} {a : R} [] [] (ha : a 0) (n : ) :
Polynomial.roots (↑() a) = n {0}
theorem Polynomial.roots_prod_X_sub_C {R : Type u} [] [] (s : ) :
Polynomial.roots (Finset.prod s fun a => Polynomial.X - Polynomial.C a) = s.val
@[simp]
theorem Polynomial.roots_multiset_prod_X_sub_C {R : Type u} [] [] (s : ) :
Polynomial.roots (Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s)) = s
@[simp]
theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card {R : Type u} [] [] (s : ) :
Polynomial.natDegree (Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s)) = Multiset.card s
theorem Polynomial.card_roots_X_pow_sub_C {R : Type u} [] [] {n : } (hn : 0 < n) (a : R) :
Multiset.card (Polynomial.roots (Polynomial.X ^ n - Polynomial.C a)) n
def Polynomial.nthRoots {R : Type u} [] [] (n : ) (a : R) :

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

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

Instances For
theorem Polynomial.nthRootsFinset_def (n : ) (R : Type u_1) [] [] [] :
@[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.Monic.comp {R : Type u} [] [] {p : } {q : } (hp : ) (hq : ) (h : ) :
theorem Polynomial.Monic.comp_X_add_C {R : Type u} [] [] {p : } (hp : ) (r : R) :
Polynomial.Monic (Polynomial.comp p (Polynomial.X + Polynomial.C r))
theorem Polynomial.Monic.comp_X_sub_C {R : Type u} [] [] {p : } (hp : ) (r : R) :
Polynomial.Monic (Polynomial.comp p (Polynomial.X - Polynomial.C r))
theorem Polynomial.units_coeff_zero_smul {R : Type u} [] [] (c : ()ˣ) (p : ) :
Polynomial.coeff (c) 0 p = c * p
@[simp]
theorem Polynomial.natDegree_coe_units {R : Type u} [] [] (u : ()ˣ) :
theorem Polynomial.comp_eq_zero_iff {R : Type u} [] [] {p : } {q : } :
= 0 p = 0 = 0 q = Polynomial.C ()
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
@[inline, reducible]
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.

Instances For
theorem Polynomial.aroots_def {T : Type w} [] (p : ) (S : Type u_1) [] [] [Algebra T S] :
theorem Polynomial.mem_aroots' {S : Type v} {T : Type w} [] [] [] [Algebra T S] {p : } {a : S} :
a Polynomial.map () p 0 ↑() p = 0
theorem Polynomial.mem_aroots {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {p : } {a : S} :
a p 0 ↑() p = 0
theorem Polynomial.aroots_mul {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {p : } {q : } (hpq : p * q 0) :
@[simp]
theorem Polynomial.aroots_X_sub_C {S : Type v} {T : Type w} [] [] [] [Algebra T S] (r : T) :
Polynomial.aroots (Polynomial.X - Polynomial.C r) S = {↑() r}
@[simp]
theorem Polynomial.aroots_X {S : Type v} {T : Type w} [] [] [] [Algebra T S] :
Polynomial.aroots Polynomial.X S = {0}
@[simp]
theorem Polynomial.aroots_C {S : Type v} {T : Type w} [] [] [] [Algebra T S] (a : T) :
Polynomial.aroots (Polynomial.C a) 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_C_mul {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {a : T} (p : ) (ha : a 0) :
Polynomial.aroots (Polynomial.C a * p) S =
@[simp]
theorem Polynomial.aroots_smul_nonzero {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {a : T} (p : ) (ha : a 0) :
@[simp]
theorem Polynomial.aroots_pow {S : Type v} {T : Type w} [] [] [] [Algebra T S] (p : ) (n : ) :
theorem Polynomial.aroots_X_pow {S : Type v} {T : Type w} [] [] [] [Algebra T S] (n : ) :
Polynomial.aroots (Polynomial.X ^ n) 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.aroots (Polynomial.C a * Polynomial.X ^ n) S = n {0}
@[simp]
theorem Polynomial.aroots_monomial {S : Type v} {T : Type w} [] [] [] [Algebra T S] [] {a : T} (ha : a 0) (n : ) :
Polynomial.aroots (↑() a) 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.

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

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 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 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 = 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) () ()
theorem Polynomial.ne_zero_of_mem_rootSet {S : Type v} {T : Type w} [] {p : } [] [] [Algebra T S] {a : S} (h : a ) :
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 = 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) () ()
theorem Polynomial.degree_eq_degree_of_associated {R : Type u} [] [] {p : } {q : } (h : ) :
theorem Polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [] [] {p : } (hi : ) {x : R} (hx : ) :
theorem Polynomial.leadingCoeff_divByMonic_of_monic {R : Type u} [] {p : } {q : } (hmonic : ) (hdegree : ) :

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

theorem Polynomial.leadingCoeff_divByMonic_X_sub_C {R : Type u} [] [] (p : ) (hp : ) (a : R) :
Polynomial.leadingCoeff (p /ₘ (Polynomial.X - Polynomial.C a)) =
theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [] {p : } {q : } (hp : ) (hdiv : p q) (hdeg : ) :
q = Polynomial.C () * p
theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [] {p : } {q : } (hp : ) (hq : ) (hdiv : p q) (hdeg : ) :
q = p
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 => Polynomial.X - Polynomial.C (s i))
theorem Polynomial.monic_prod_multiset_X_sub_C {R : Type u} [] [] {p : } :
Polynomial.Monic (Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ()))
theorem Polynomial.prod_multiset_root_eq_finset_root {R : Type u} [] [] {p : } [] :
Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ()) = Finset.prod () fun a => (Polynomial.X - Polynomial.C a) ^
theorem Polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [] [] (p : ) :
Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ()) 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.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s) p

A Galois connection.

theorem Polynomial.exists_prod_multiset_X_sub_C_mul {R : Type u} [] [] (p : ) :
q, Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ()) * q = p Multiset.card () + =
theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C {R : Type u} [] [] {p : } (hroots : Multiset.card () = ) :
Polynomial.C () * Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ()) = 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 : ) (hroots : Multiset.card () = ) :
Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ()) = 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.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) :
theorem Polynomial.count_map_roots_of_injective {A : Type u_1} {B : Type u_2} [] [] [] [] (p : ) {f : A →+* B} (hf : ) (b : B) :
theorem Polynomial.map_roots_le {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (h : 0) :
Multiset.map (f) ()
theorem Polynomial.map_roots_le_of_injective {A : Type u_1} {B : Type u_2} [] [] [] [] (p : ) {f : A →+* B} (hf : ) :
Multiset.map (f) ()
theorem Polynomial.card_roots_le_map {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (h : 0) :
Multiset.card () Multiset.card ()
theorem Polynomial.card_roots_le_map_of_injective {A : Type u_1} {B : Type u_2} [] [] [] [] {p : } {f : A →+* B} (hf : ) :
Multiset.card () Multiset.card ()
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 () = ) :
Multiset.map (f) () =
theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map {R : Type u} {S : Type v} [] [] [] (φ : R →+* S) {f : } (hf : ) (H : IsUnit ()) :
theorem Polynomial.Monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [] [] [] [] (φ : R →+* S) (f : ) (h_mon : ) (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.