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} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p ≠ 0) {z : S} (hz : (Polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) : 0 < Polynomial.natDegree p

theorem Polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p ≠ 0) {z : S} (hz : (Polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) : 0 < Polynomial.degree p

theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [CommRing R] {q : Polynomial R} (hq : Polynomial.Monic q) {p₁ : Polynomial R} {p₂ : Polynomial R} (h : q ∣ p₁ - p₂) : p₁ %ₘ q = p₂ %ₘ q

theorem Polynomial.add_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (p₁ : Polynomial R) (p₂ : Polynomial R) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

theorem Polynomial.smul_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (c : R) (p : Polynomial R) : c • p %ₘ q = c • (p %ₘ q)

@[simp]

theorem Polynomial.modByMonicHom_apply {R : Type u} [CommRing R] (q : Polynomial R) (p : Polynomial R) : (Polynomial.modByMonicHom q) p = p %ₘ q

def Polynomial.modByMonicHom {R : Type u} [CommRing R] (q : Polynomial R) : Polynomial R →ₗ[R] Polynomial R

_ %ₘ q as an R-linear map.

Equations

• Polynomial.modByMonicHom q = { toAddHom := { toFun := fun (p : Polynomial R) => p %ₘ q, map_add' := ⋯ }, map_smul' := ⋯ }

theorem Polynomial.neg_modByMonic {R : Type u} [CommRing R] (p : Polynomial R) (mod : Polynomial R) : -p %ₘ mod = -(p %ₘ mod)

theorem Polynomial.sub_modByMonic {R : Type u} [CommRing R] (a : Polynomial R) (b : Polynomial R) (mod : Polynomial R) : (a - b) %ₘ mod = a %ₘ mod - b %ₘ mod

theorem Polynomial.aeval_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) {x : S} (hx : (Polynomial.aeval x) q = 0) : (Polynomial.aeval x) (p %ₘ q) = (Polynomial.aeval x) p

instance Polynomial.instNoZeroDivisorsPolynomialMul'Zero {R : Type u} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (Polynomial R)

Equations

• ⋯ = ⋯

theorem Polynomial.natDegree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (hp : p ≠ 0) (hq : q ≠ 0) : Polynomial.natDegree (p * q) = Polynomial.natDegree p + Polynomial.natDegree q

theorem Polynomial.trailingDegree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} : Polynomial.trailingDegree (p * q) = Polynomial.trailingDegree p + Polynomial.trailingDegree q

@[simp]

theorem Polynomial.natDegree_pow {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ℕ) : Polynomial.natDegree (p ^ n) = n * Polynomial.natDegree p

theorem Polynomial.degree_le_mul_left {R : Type u} [Semiring R] [NoZeroDivisors R] {q : Polynomial R} (p : Polynomial R) (hq : q ≠ 0) : Polynomial.degree p ≤ Polynomial.degree (p * q)

theorem Polynomial.natDegree_le_of_dvd {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h1 : p ∣ q) (h2 : q ≠ 0) : Polynomial.natDegree p ≤ Polynomial.natDegree q

theorem Polynomial.degree_le_of_dvd {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h1 : p ∣ q) (h2 : q ≠ 0) : Polynomial.degree p ≤ Polynomial.degree q

theorem Polynomial.eq_zero_of_dvd_of_degree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h₁ : p ∣ q) (h₂ : Polynomial.degree q < Polynomial.degree p) : q = 0

theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h₁ : p ∣ q) (h₂ : Polynomial.natDegree q < Polynomial.natDegree p) : q = 0

theorem Polynomial.not_dvd_of_degree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h0 : q ≠ 0) (hl : Polynomial.degree q < Polynomial.degree p) : ¬p ∣ q

theorem Polynomial.not_dvd_of_natDegree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h0 : q ≠ 0) (hl : Polynomial.natDegree q < Polynomial.natDegree p) : ¬p ∣ q

theorem Polynomial.natDegree_sub_eq_of_prod_eq {R : Type u} [Semiring R] [NoZeroDivisors R] {p₁ : Polynomial R} {p₂ : Polynomial R} {q₁ : Polynomial R} {q₂ : Polynomial R} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0) (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0) (h_eq : p₁ * q₂ = p₂ * q₁) : ↑(Polynomial.natDegree p₁) - ↑(Polynomial.natDegree q₁) = ↑(Polynomial.natDegree p₂) - ↑(Polynomial.natDegree q₂)

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

theorem Polynomial.natDegree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} (h : IsUnit p) : Polynomial.natDegree p = 0

theorem Polynomial.degree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} [Nontrivial R] (h : IsUnit p) : Polynomial.degree p = 0

@[simp]

theorem Polynomial.degree_coe_units {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) : Polynomial.degree ↑u = 0

theorem Polynomial.isUnit_iff {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} : IsUnit p ↔ ∃ (r : R), IsUnit 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} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < Polynomial.degree p) : ¬IsUnit p

theorem Polynomial.not_isUnit_of_natDegree_pos {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < Polynomial.natDegree p) : ¬IsUnit p

theorem Polynomial.irreducible_of_monic {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : Polynomial.Monic p) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (f g : Polynomial R), Polynomial.Monic f → Polynomial.Monic g → f * g = p → f = 1 ∨ g = 1

theorem Polynomial.Monic.irreducible_iff_natDegree {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : Polynomial.Monic p) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), Polynomial.Monic f → Polynomial.Monic g → f * g = p → Polynomial.natDegree f = 0 ∨ Polynomial.natDegree g = 0

theorem Polynomial.Monic.irreducible_iff_natDegree' {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : Polynomial.Monic p) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), Polynomial.Monic f → Polynomial.Monic g → f * g = p → Polynomial.natDegree g ∉ Finset.Ioc 0 (Polynomial.natDegree p / 2)

theorem Polynomial.Monic.irreducible_iff_lt_natDegree_lt {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : Polynomial.Monic p) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (q : Polynomial R), Polynomial.Monic q → Polynomial.natDegree q ∈ Finset.Ioc 0 (Polynomial.natDegree p / 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} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hm : Polynomial.Monic p) (hnd : Polynomial.natDegree p = 2) : ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), Polynomial.coeff p 0 = c₁ * c₂ ∧ Polynomial.coeff p 1 = c₁ + c₂

theorem Polynomial.root_mul {R : Type u} {a : R} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} : Polynomial.IsRoot (p * q) a ↔ Polynomial.IsRoot p a ∨ Polynomial.IsRoot q a

theorem Polynomial.root_or_root_of_root_mul {R : Type u} {a : R} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h : Polynomial.IsRoot (p * q) a) : Polynomial.IsRoot p a ∨ Polynomial.IsRoot q a

instance Polynomial.instIsDomainPolynomialToSemiringSemiring {R : Type u} [Ring R] [IsDomain R] : IsDomain (Polynomial R)

Equations

• ⋯ = ⋯

theorem Polynomial.Monic.C_dvd_iff_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : Polynomial.Monic p) {a : R} : Polynomial.C a ∣ p ↔ IsUnit a

theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [CommSemiring R] {a : Polynomial R} {p : Polynomial R} (ha : ¬IsUnit a) (hap : a ∣ p) (hp : Polynomial.Monic p) : 0 < Polynomial.degree a

theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [CommSemiring R] {a : Polynomial R} {p : Polynomial R} (ha : ¬IsUnit a) (hap : a ∣ p) (hp : Polynomial.Monic p) : 0 < Polynomial.natDegree a

theorem Polynomial.degree_pos_of_monic_of_not_isUnit {R : Type u} [CommSemiring R] {a : Polynomial R} (hu : ¬IsUnit a) (ha : Polynomial.Monic a) : 0 < Polynomial.degree a

theorem Polynomial.natDegree_pos_of_monic_of_not_isUnit {R : Type u} [CommSemiring R] {a : Polynomial R} (hu : ¬IsUnit a) (ha : Polynomial.Monic a) : 0 < Polynomial.natDegree a

theorem Polynomial.le_rootMultiplicity_iff {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p ≠ 0) {a : R} {n : ℕ} : n ≤ Polynomial.rootMultiplicity a p ↔ (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} [CommRing R] {p : Polynomial R} (p0 : p ≠ 0) (a : R) (n : ℕ) : Polynomial.rootMultiplicity a p ≤ n ↔ ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p

theorem Polynomial.pow_rootMultiplicity_not_dvd {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p ≠ 0) (a : R) : ¬(Polynomial.X - Polynomial.C a) ^ (Polynomial.rootMultiplicity a p + 1) ∣ p

theorem Polynomial.X_sub_C_pow_dvd_iff {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} : (Polynomial.X - Polynomial.C t) ^ n ∣ p ↔ Polynomial.X ^ n ∣ Polynomial.comp p (Polynomial.X + Polynomial.C t)

theorem Polynomial.comp_X_add_C_eq_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} (t : R) : Polynomial.comp p (Polynomial.X + Polynomial.C t) = 0 ↔ p = 0

theorem Polynomial.comp_X_add_C_ne_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} (t : R) : Polynomial.comp p (Polynomial.X + Polynomial.C t) ≠ 0 ↔ p ≠ 0

theorem Polynomial.rootMultiplicity_eq_rootMultiplicity {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.rootMultiplicity t p = Polynomial.rootMultiplicity 0 (Polynomial.comp p (Polynomial.X + Polynomial.C t))

theorem Polynomial.rootMultiplicity_eq_natTrailingDegree' {R : Type u} [CommRing R] {p : Polynomial R} : Polynomial.rootMultiplicity 0 p = Polynomial.natTrailingDegree p

theorem Polynomial.rootMultiplicity_eq_natTrailingDegree {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.rootMultiplicity t p = Polynomial.natTrailingDegree (Polynomial.comp p (Polynomial.X + Polynomial.C t))

theorem Polynomial.eval_divByMonic_eq_trailingCoeff_comp {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p) = Polynomial.trailingCoeff (Polynomial.comp p (Polynomial.X + Polynomial.C t))

theorem Polynomial.Monic.mem_nonZeroDivisors {R : Type u} [CommRing R] {p : Polynomial R} (h : Polynomial.Monic p) : p ∈ nonZeroDivisors (Polynomial R)

theorem Polynomial.mem_nonZeroDivisors_of_leadingCoeff {R : Type u} [CommRing R] {p : Polynomial R} (h : Polynomial.leadingCoeff p ∈ nonZeroDivisors R) : p ∈ nonZeroDivisors (Polynomial R)

theorem Polynomial.rootMultiplicity_mul_X_sub_C_pow {R : Type u} [CommRing R] {p : Polynomial R} {a : R} {n : ℕ} (h : p ≠ 0) : Polynomial.rootMultiplicity a (p * (Polynomial.X - Polynomial.C a) ^ n) = Polynomial.rootMultiplicity a p + n

theorem Polynomial.rootMultiplicity_X_sub_C_pow {R : Type u} [CommRing R] [Nontrivial R] (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} [CommRing R] [Nontrivial R] {x : R} : Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C x) = 1

theorem Polynomial.rootMultiplicity_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] [DecidableEq R] {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} [CommRing R] {p : Polynomial R} {q : Polynomial R} (a : R) (hzero : p + q ≠ 0) : min (Polynomial.rootMultiplicity a p) (Polynomial.rootMultiplicity a q) ≤ Polynomial.rootMultiplicity a (p + q)

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

theorem Polynomial.le_rootMultiplicity_mul {R : Type u} [CommRing R] {p : Polynomial R} {q : Polynomial R} (x : R) (hpq : p * q ≠ 0) : Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q ≤ Polynomial.rootMultiplicity x (p * q)

theorem Polynomial.rootMultiplicity_mul' {R : Type u} [CommRing R] {p : Polynomial R} {q : Polynomial R} {x : R} (hpq : Polynomial.eval x (p /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x p) * Polynomial.eval x (q /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x q) ≠ 0) : Polynomial.rootMultiplicity x (p * q) = Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q

theorem Polynomial.prime_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) : Prime (Polynomial.X - Polynomial.C r)

theorem Polynomial.prime_X {R : Type u} [CommRing R] [IsDomain R] : Prime Polynomial.X

theorem Polynomial.Monic.prime_of_degree_eq_one {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : Polynomial.degree p = 1) (hm : Polynomial.Monic p) : Prime p

theorem Polynomial.irreducible_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) : Irreducible (Polynomial.X - Polynomial.C r)

theorem Polynomial.irreducible_X {R : Type u} [CommRing R] [IsDomain R] : Irreducible Polynomial.X

theorem Polynomial.Monic.irreducible_of_degree_eq_one {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : Polynomial.degree p = 1) (hm : Polynomial.Monic p) : Irreducible p

theorem Polynomial.rootMultiplicity_mul {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} {x : R} (hpq : p * q ≠ 0) : Polynomial.rootMultiplicity x (p * q) = Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q

theorem Polynomial.exists_multiset_roots {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} : p ≠ 0 → ∃ (s : Multiset R), ↑(Multiset.card s) ≤ Polynomial.degree p ∧ ∀ (a : R), Multiset.count a s = Polynomial.rootMultiplicity a p

noncomputable def Polynomial.roots {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : Multiset R

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

Equations

• Polynomial.roots p = if h : p = 0 then ∅ else Classical.choose ⋯

theorem Polynomial.roots_def {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] (p : Polynomial R) [Decidable (p = 0)] : Polynomial.roots p = if h : p = 0 then ∅ else Classical.choose ⋯

@[simp]

theorem Polynomial.roots_zero {R : Type u} [CommRing R] [IsDomain R] : Polynomial.roots 0 = 0

theorem Polynomial.card_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp0 : p ≠ 0) : ↑(Multiset.card (Polynomial.roots p)) ≤ Polynomial.degree p

theorem Polynomial.card_roots' {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : Multiset.card (Polynomial.roots p) ≤ Polynomial.natDegree p

theorem Polynomial.card_roots_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < Polynomial.degree p) : ↑(Multiset.card (Polynomial.roots (p - Polynomial.C a))) ≤ Polynomial.degree p

theorem Polynomial.card_roots_sub_C' {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < Polynomial.degree p) : Multiset.card (Polynomial.roots (p - Polynomial.C a)) ≤ Polynomial.natDegree p

@[simp]

theorem Polynomial.count_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] [DecidableEq R] (p : Polynomial R) : Multiset.count a (Polynomial.roots p) = Polynomial.rootMultiplicity a p

@[simp]

theorem Polynomial.mem_roots' {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} : a ∈ Polynomial.roots p ↔ p ≠ 0 ∧ Polynomial.IsRoot p a

theorem Polynomial.mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : a ∈ Polynomial.roots p ↔ Polynomial.IsRoot p a

theorem Polynomial.ne_zero_of_mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (h : a ∈ Polynomial.roots p) : p ≠ 0

theorem Polynomial.isRoot_of_mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (h : a ∈ Polynomial.roots p) : Polynomial.IsRoot p a

theorem Polynomial.mem_roots_iff_aeval_eq_zero {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {x : R} (w : p ≠ 0) : x ∈ Polynomial.roots p ↔ (Polynomial.aeval x) p = 0

theorem Polynomial.card_le_degree_of_subset_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {Z : Finset R} (h : Z.val ⊆ Polynomial.roots p) : Z.card ≤ Polynomial.natDegree p

theorem Polynomial.finite_setOf_isRoot {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : Set.Finite {x : R | Polynomial.IsRoot p x}

theorem Polynomial.eq_zero_of_infinite_isRoot {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (h : Set.Infinite {x : R | Polynomial.IsRoot p x}) : p = 0

theorem Polynomial.exists_max_root {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p ≠ 0) : ∃ (x₀ : R), ∀ (x : R), Polynomial.IsRoot p x → x ≤ x₀

theorem Polynomial.exists_min_root {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p ≠ 0) : ∃ (x₀ : R), ∀ (x : R), Polynomial.IsRoot p x → x₀ ≤ x

theorem Polynomial.eq_of_infinite_eval_eq {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (q : Polynomial R) (h : Set.Infinite {x : R | Polynomial.eval x p = Polynomial.eval x q}) : p = q

theorem Polynomial.roots_mul {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hpq : p * q ≠ 0) : Polynomial.roots (p * q) = Polynomial.roots p + Polynomial.roots q

theorem Polynomial.roots.le_of_dvd {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (h : q ≠ 0) : p ∣ q → Polynomial.roots p ≤ Polynomial.roots q

theorem Polynomial.mem_roots_sub_C' {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} {x : R} : x ∈ Polynomial.roots (p - Polynomial.C a) ↔ p ≠ Polynomial.C a ∧ Polynomial.eval x p = a

theorem Polynomial.mem_roots_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} {x : R} (hp0 : 0 < Polynomial.degree p) : x ∈ Polynomial.roots (p - Polynomial.C a) ↔ Polynomial.eval x p = a

@[simp]

theorem Polynomial.roots_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) : Polynomial.roots (Polynomial.X - Polynomial.C r) = {r}

@[simp]

theorem Polynomial.roots_X {R : Type u} [CommRing R] [IsDomain R] : Polynomial.roots Polynomial.X = {0}

@[simp]

theorem Polynomial.roots_C {R : Type u} [CommRing R] [IsDomain R] (x : R) : Polynomial.roots (Polynomial.C x) = 0

@[simp]

theorem Polynomial.roots_one {R : Type u} [CommRing R] [IsDomain R] : Polynomial.roots 1 = ∅

@[simp]

theorem Polynomial.roots_C_mul {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a ≠ 0) : Polynomial.roots (Polynomial.C a * p) = Polynomial.roots p

@[simp]

theorem Polynomial.roots_smul_nonzero {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a ≠ 0) : Polynomial.roots (a • p) = Polynomial.roots p

@[simp]

theorem Polynomial.roots_neg {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : Polynomial.roots (-p) = Polynomial.roots p

theorem Polynomial.roots_list_prod {R : Type u} [CommRing R] [IsDomain R] (L : List (Polynomial R)) : 0 ∉ L → Polynomial.roots (List.prod L) = Multiset.bind (↑L) Polynomial.roots

theorem Polynomial.roots_multiset_prod {R : Type u} [CommRing R] [IsDomain R] (m : Multiset (Polynomial R)) : 0 ∉ m → Polynomial.roots (Multiset.prod m) = Multiset.bind m Polynomial.roots

theorem Polynomial.roots_prod {R : Type u} [CommRing R] [IsDomain R] {ι : Type u_1} (f : ι → Polynomial R) (s : Finset ι) : Finset.prod s f ≠ 0 → Polynomial.roots (Finset.prod s f) = Multiset.bind s.val fun (i : ι) => Polynomial.roots (f i)

@[simp]

theorem Polynomial.roots_pow {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (n : ℕ) : Polynomial.roots (p ^ n) = n • Polynomial.roots p

theorem Polynomial.roots_X_pow {R : Type u} [CommRing R] [IsDomain R] (n : ℕ) : Polynomial.roots (Polynomial.X ^ n) = n • {0}

theorem Polynomial.roots_C_mul_X_pow {R : Type u} {a : R} [CommRing R] [IsDomain 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} [CommRing R] [IsDomain R] (ha : a ≠ 0) (n : ℕ) : Polynomial.roots ((Polynomial.monomial n) a) = n • {0}

theorem Polynomial.roots_prod_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (s : Finset R) : Polynomial.roots (Finset.prod s fun (a : R) => Polynomial.X - Polynomial.C a) = s.val

@[simp]

theorem Polynomial.roots_multiset_prod_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) : Polynomial.roots (Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s)) = s

@[simp]

theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) : Polynomial.natDegree (Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s)) = Multiset.card s

theorem Polynomial.card_roots_X_pow_sub_C {R : Type u} [CommRing R] [IsDomain R] {n : ℕ} (hn : 0 < n) (a : R) : Multiset.card (Polynomial.roots (Polynomial.X ^ n - Polynomial.C a)) ≤ n

def Polynomial.nthRoots {R : Type u} [CommRing R] [IsDomain R] (n : ℕ) (a : R) : Multiset R

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

Equations

• Polynomial.nthRoots n a = Polynomial.roots (Polynomial.X ^ n - Polynomial.C a)

@[simp]

theorem Polynomial.mem_nthRoots {R : Type u} [CommRing R] [IsDomain R] {n : ℕ} (hn : 0 < n) {a : R} {x : R} : x ∈ Polynomial.nthRoots n a ↔ x ^ n = a

@[simp]

theorem Polynomial.nthRoots_zero {R : Type u} [CommRing R] [IsDomain R] (r : R) : Polynomial.nthRoots 0 r = 0

@[simp]

theorem Polynomial.nthRoots_zero_right {R : Type u_1} [CommRing R] [IsDomain R] (n : ℕ) : Polynomial.nthRoots n 0 = Multiset.replicate n 0

theorem Polynomial.card_nthRoots {R : Type u} [CommRing R] [IsDomain R] (n : ℕ) (a : R) : Multiset.card (Polynomial.nthRoots n a) ≤ n

@[simp]

theorem Polynomial.nthRoots_two_eq_zero_iff {R : Type u} [CommRing R] [IsDomain R] {r : R} : Polynomial.nthRoots 2 r = 0 ↔ ¬IsSquare r

def Polynomial.nthRootsFinset (n : ℕ) (R : Type u_1) [CommRing R] [IsDomain R] : Finset R

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

Equations

• Polynomial.nthRootsFinset n R = Multiset.toFinset (Polynomial.nthRoots n 1)

theorem Polynomial.nthRootsFinset_def (n : ℕ) (R : Type u_1) [CommRing R] [IsDomain R] [DecidableEq R] : Polynomial.nthRootsFinset n R = Multiset.toFinset (Polynomial.nthRoots n 1)

@[simp]

theorem Polynomial.mem_nthRootsFinset {R : Type u} [CommRing R] [IsDomain R] {n : ℕ} (h : 0 < n) {x : R} : x ∈ Polynomial.nthRootsFinset n R ↔ x ^ n = 1

@[simp]

theorem Polynomial.nthRootsFinset_zero {R : Type u} [CommRing R] [IsDomain R] : Polynomial.nthRootsFinset 0 R = ∅

theorem Polynomial.mul_mem_nthRootsFinset {R : Type u} {n : ℕ} [CommRing R] [IsDomain R] {η₁ : R} {η₂ : R} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset n R) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset n R) : η₁ * η₂ ∈ Polynomial.nthRootsFinset n R

theorem Polynomial.ne_zero_of_mem_nthRootsFinset {R : Type u} {n : ℕ} [CommRing R] [IsDomain R] {η : R} (hη : η ∈ Polynomial.nthRootsFinset n R) : η ≠ 0

theorem Polynomial.one_mem_nthRootsFinset {R : Type u} {n : ℕ} [CommRing R] [IsDomain R] (hn : 0 < n) : 1 ∈ Polynomial.nthRootsFinset n R

theorem Polynomial.Monic.comp {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : Polynomial.Monic q) (h : Polynomial.natDegree q ≠ 0) : Polynomial.Monic (Polynomial.comp p q)

theorem Polynomial.Monic.comp_X_add_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : Polynomial.Monic p) (r : R) : Polynomial.Monic (Polynomial.comp p (Polynomial.X + Polynomial.C r))

theorem Polynomial.Monic.comp_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : Polynomial.Monic p) (r : R) : Polynomial.Monic (Polynomial.comp p (Polynomial.X - Polynomial.C r))

theorem Polynomial.units_coeff_zero_smul {R : Type u} [CommRing R] [IsDomain R] (c : (Polynomial R)ˣ) (p : Polynomial R) : Polynomial.coeff (↑c) 0 • p = ↑c * p

@[simp]

theorem Polynomial.natDegree_coe_units {R : Type u} [CommRing R] [IsDomain R] (u : (Polynomial R)ˣ) : Polynomial.natDegree ↑u = 0

theorem Polynomial.comp_eq_zero_iff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} : Polynomial.comp p q = 0 ↔ p = 0 ∨ Polynomial.eval (Polynomial.coeff q 0) p = 0 ∧ q = Polynomial.C (Polynomial.coeff q 0)

theorem Polynomial.zero_of_eval_zero {R : Type u} [CommRing R] [IsDomain R] [Infinite R] (p : Polynomial R) (h : ∀ (x : R), Polynomial.eval x p = 0) : p = 0

theorem Polynomial.funext {R : Type u} [CommRing R] [IsDomain R] [Infinite R] {p : Polynomial R} {q : Polynomial R} (ext : ∀ (r : R), Polynomial.eval r p = Polynomial.eval r q) : p = q

@[inline, reducible]

noncomputable abbrev Polynomial.aroots {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Multiset 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

• Polynomial.aroots p S = Polynomial.roots (Polynomial.map (algebraMap T S) p)

theorem Polynomial.aroots_def {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Polynomial.aroots p S = Polynomial.roots (Polynomial.map (algebraMap T S) p)

theorem Polynomial.mem_aroots' {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {p : Polynomial T} {a : S} : a ∈ Polynomial.aroots p S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0

theorem Polynomial.mem_aroots {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p : Polynomial T} {a : S} : a ∈ Polynomial.aroots p S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0

theorem Polynomial.aroots_mul {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p : Polynomial T} {q : Polynomial T} (hpq : p * q ≠ 0) : Polynomial.aroots (p * q) S = Polynomial.aroots p S + Polynomial.aroots q S

@[simp]

theorem Polynomial.aroots_X_sub_C {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (r : T) : Polynomial.aroots (Polynomial.X - Polynomial.C r) S = {(algebraMap T S) r}

@[simp]

theorem Polynomial.aroots_X {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] : Polynomial.aroots Polynomial.X S = {0}

@[simp]

theorem Polynomial.aroots_C {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (a : T) : Polynomial.aroots (Polynomial.C a) S = 0

@[simp]

theorem Polynomial.aroots_zero {T : Type w} [CommRing T] (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Polynomial.aroots 0 S = 0

@[simp]

theorem Polynomial.aroots_one {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] : Polynomial.aroots 1 S = 0

@[simp]

theorem Polynomial.aroots_neg {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (p : Polynomial T) : Polynomial.aroots (-p) S = Polynomial.aroots p S

@[simp]

theorem Polynomial.aroots_C_mul {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : Polynomial T) (ha : a ≠ 0) : Polynomial.aroots (Polynomial.C a * p) S = Polynomial.aroots p S

@[simp]

theorem Polynomial.aroots_smul_nonzero {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : Polynomial T) (ha : a ≠ 0) : Polynomial.aroots (a • p) S = Polynomial.aroots p S

@[simp]

theorem Polynomial.aroots_pow {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (p : Polynomial T) (n : ℕ) : Polynomial.aroots (p ^ n) S = n • Polynomial.aroots p S

theorem Polynomial.aroots_X_pow {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [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} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors 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} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) : Polynomial.aroots ((Polynomial.monomial n) a) S = n • {0}

def Polynomial.rootSet {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [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

• Polynomial.rootSet p S = ↑(Multiset.toFinset (Polynomial.aroots p S))

theorem Polynomial.rootSet_def {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] [DecidableEq S] : Polynomial.rootSet p S = ↑(Multiset.toFinset (Polynomial.aroots p S))

@[simp]

theorem Polynomial.rootSet_C {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (a : T) : Polynomial.rootSet (Polynomial.C a) S = ∅

@[simp]

theorem Polynomial.rootSet_zero {T : Type w} [CommRing T] (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Polynomial.rootSet 0 S = ∅

@[simp]

theorem Polynomial.rootSet_one {T : Type w} [CommRing T] (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Polynomial.rootSet 1 S = ∅

@[simp]

theorem Polynomial.rootSet_neg {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Polynomial.rootSet (-p) S = Polynomial.rootSet p S

instance Polynomial.rootSetFintype {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Fintype ↑(Polynomial.rootSet p S)

Equations

• Polynomial.rootSetFintype p S = FinsetCoe.fintype (Multiset.toFinset (Polynomial.aroots p S))

theorem Polynomial.rootSet_finite {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : Set.Finite (Polynomial.rootSet p S)

theorem Polynomial.bUnion_roots_finite {R : Type u_1} {S : Type u_2} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S] (m : R →+* S) (d : ℕ) {U : Set R} (h : Set.Finite U) : Set.Finite (⋃ (f : Polynomial R), ⋃ (_ : Polynomial.natDegree f ≤ d ∧ ∀ (i : ℕ), Polynomial.coeff f i ∈ U), ↑(Multiset.toFinset (Polynomial.roots (Polynomial.map m f))))

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} [CommRing T] {p : Polynomial T} {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] {a : S} : a ∈ Polynomial.rootSet p S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0

theorem Polynomial.mem_rootSet {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : S} : a ∈ Polynomial.rootSet p S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0

theorem Polynomial.mem_rootSet_of_ne {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] (hp : p ≠ 0) {a : S} : a ∈ Polynomial.rootSet p S ↔ (Polynomial.aeval a) p = 0

theorem Polynomial.rootSet_maps_to' {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} {S' : Type u_2} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S'] (hp : Polynomial.map (algebraMap T S') p = 0 → Polynomial.map (algebraMap T S) p = 0) (f : S →ₐ[T] S') : Set.MapsTo (⇑f) (Polynomial.rootSet p S) (Polynomial.rootSet p S')

theorem Polynomial.ne_zero_of_mem_rootSet {S : Type v} {T : Type w} [CommRing T] {p : Polynomial T} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (h : a ∈ Polynomial.rootSet p S) : p ≠ 0

theorem Polynomial.aeval_eq_zero_of_mem_rootSet {S : Type v} {T : Type w} [CommRing T] {p : Polynomial T} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (hx : a ∈ Polynomial.rootSet p S) : (Polynomial.aeval a) p = 0

theorem Polynomial.rootSet_mapsTo {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} {S' : Type u_2} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S'] [NoZeroSMulDivisors T S'] (f : S →ₐ[T] S') : Set.MapsTo (⇑f) (Polynomial.rootSet p S) (Polynomial.rootSet p S')

theorem Polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [CommRing R] [IsDomain R] (u : (Polynomial R)ˣ) : Polynomial.coeff (↑u) 0 ≠ 0

theorem Polynomial.degree_eq_degree_of_associated {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (h : Associated p q) : Polynomial.degree p = Polynomial.degree q

theorem Polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hi : Irreducible p) {x : R} (hx : Polynomial.IsRoot p x) : Polynomial.degree p = 1

theorem Polynomial.leadingCoeff_divByMonic_of_monic {R : Type u} [CommRing R] {p : Polynomial R} {q : Polynomial R} (hmonic : Polynomial.Monic q) (hdegree : Polynomial.degree q ≤ Polynomial.degree p) : Polynomial.leadingCoeff (p /ₘ q) = Polynomial.leadingCoeff p

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

theorem Polynomial.leadingCoeff_divByMonic_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (hp : Polynomial.degree p ≠ 0) (a : R) : Polynomial.leadingCoeff (p /ₘ (Polynomial.X - Polynomial.C a)) = Polynomial.leadingCoeff p

theorem Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hpq : p ∣ q) (h₁ : Polynomial.natDegree q ≤ Polynomial.natDegree p) (h₂ : Polynomial.leadingCoeff p = Polynomial.leadingCoeff q) : p = q

theorem Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hpq : p ∣ q) (h₁ : Polynomial.natDegree q ≤ Polynomial.natDegree p) (h₂ : Polynomial.leadingCoeff q ∣ Polynomial.leadingCoeff p) : Associated p q

theorem Polynomial.associated_of_dvd_of_natDegree_le {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hpq : p ∣ q) (hq : q ≠ 0) (h₁ : Polynomial.natDegree q ≤ Polynomial.natDegree p) : Associated p q

theorem Polynomial.associated_of_dvd_of_degree_eq {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hpq : p ∣ q) (h₁ : Polynomial.degree p = Polynomial.degree q) : Associated p q

theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [CommRing R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hdiv : p ∣ q) (hdeg : Polynomial.natDegree q ≤ Polynomial.natDegree p) : q = Polynomial.C (Polynomial.leadingCoeff q) * p

theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [CommRing R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : Polynomial.Monic q) (hdiv : p ∣ q) (hdeg : Polynomial.natDegree q ≤ Polynomial.natDegree p) : q = p

theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] (p : Polynomial R) {ι : Type u_2} [Fintype ι] {f : ι → R} (hf : Function.Injective f) (heval : ∀ (i : ι), Polynomial.eval (f i) p = 0) (hcard : Polynomial.natDegree p < Fintype.card ι) : p = 0

theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' {R : Type u_1} [CommRing R] [IsDomain R] (p : Polynomial R) (s : Finset R) (heval : ∀ i ∈ s, Polynomial.eval i p = 0) (hcard : Polynomial.natDegree p < s.card) : p = 0

theorem Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_card {R : Type u} [CommRing R] [IsDomain R] (f : Polynomial R) (hf : ∀ (r : R), Polynomial.eval r f = 0) (hfR : ↑(Polynomial.natDegree f) < Cardinal.mk R) : f = 0

theorem Polynomial.exists_eval_ne_zero_of_natDegree_lt_card {R : Type u} [CommRing R] [IsDomain R] (f : Polynomial R) (hf : f ≠ 0) (hfR : ↑(Polynomial.natDegree f) < Cardinal.mk R) : ∃ (r : R), Polynomial.eval r f ≠ 0

theorem Polynomial.isCoprime_X_sub_C_of_isUnit_sub {R : Type u_1} [CommRing R] {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} [Field K] {I : Type v} {s : I → K} (H : Function.Injective s) : Pairwise (IsCoprime on fun (i : I) => Polynomial.X - Polynomial.C (s i))

theorem Polynomial.monic_prod_multiset_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} : Polynomial.Monic (Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) (Polynomial.roots p)))

theorem Polynomial.prod_multiset_root_eq_finset_root {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} [DecidableEq R] : Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) = Finset.prod (Multiset.toFinset (Polynomial.roots p)) fun (a : R) => (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p

theorem Polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) ∣ 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} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) (s : Multiset R) : Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s) ∣ p ↔ s ≤ Polynomial.roots p

A Galois connection.

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

theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : Multiset.card (Polynomial.roots p) = Polynomial.natDegree p) : Polynomial.C (Polynomial.leadingCoeff p) * Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) = 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} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : Polynomial.Monic p) (hroots : Multiset.card (Polynomial.roots p) = Polynomial.natDegree p) : Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) = 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} [CommRing R] [IsDomain R] {a : Polynomial R} {p : Polynomial R} (hp : Polynomial.Monic p) (hap : a ∣ p) : IsUnit (Polynomial.leadingCoeff a)

theorem Polynomial.Monic.irreducible_iff_degree_lt {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (p_monic : Polynomial.Monic p) (p_1 : p ≠ 1) : Irreducible p ↔ ∀ (q : Polynomial R), Polynomial.degree q ≤ ↑(Polynomial.natDegree p / 2) → q ∣ p → IsUnit q

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} [CommRing A] [CommRing B] {p : Polynomial A} {f : A →+* B} (hmap : Polynomial.map f p ≠ 0) (a : A) : Polynomial.rootMultiplicity a p ≤ Polynomial.rootMultiplicity (f a) (Polynomial.map f p)

theorem Polynomial.eq_rootMultiplicity_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) (a : A) : Polynomial.rootMultiplicity a p = Polynomial.rootMultiplicity (f a) (Polynomial.map f p)

theorem Polynomial.count_map_roots {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [DecidableEq B] {p : Polynomial A} {f : A →+* B} (hmap : Polynomial.map f p ≠ 0) (b : B) : Multiset.count b (Multiset.map (⇑f) (Polynomial.roots p)) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)

theorem Polynomial.count_map_roots_of_injective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [DecidableEq B] (p : Polynomial A) {f : A →+* B} (hf : Function.Injective ⇑f) (b : B) : Multiset.count b (Multiset.map (⇑f) (Polynomial.roots p)) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)

theorem Polynomial.map_roots_le {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : Polynomial.map f p ≠ 0) : Multiset.map (⇑f) (Polynomial.roots p) ≤ Polynomial.roots (Polynomial.map f p)

theorem Polynomial.map_roots_le_of_injective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] (p : Polynomial A) {f : A →+* B} (hf : Function.Injective ⇑f) : Multiset.map (⇑f) (Polynomial.roots p) ≤ Polynomial.roots (Polynomial.map f p)

theorem Polynomial.card_roots_le_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : Polynomial.map f p ≠ 0) : Multiset.card (Polynomial.roots p) ≤ Multiset.card (Polynomial.roots (Polynomial.map f p))

theorem Polynomial.card_roots_le_map_of_injective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) : Multiset.card (Polynomial.roots p) ≤ Multiset.card (Polynomial.roots (Polynomial.map f p))

theorem Polynomial.roots_map_of_injective_of_card_eq_natDegree {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) (hroots : Multiset.card (Polynomial.roots p) = Polynomial.natDegree p) : Multiset.map (⇑f) (Polynomial.roots p) = Polynomial.roots (Polynomial.map f p)

theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map {R : Type u} {S : Type v} [Semiring R] [CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R} (hf : IsUnit (Polynomial.leadingCoeff f)) (H : IsUnit (Polynomial.map φ f)) : IsUnit f

theorem Polynomial.Monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] (φ : R →+* S) (f : Polynomial R) (h_mon : Polynomial.Monic f) (h_irr : Irreducible (Polynomial.map φ f)) : Irreducible f

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.