Theory of univariate polynomials

We prove basic results about univariate polynomials.

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

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

theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [CommRing R] {q : Polynomial R} (hq : q.Monic) {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) : q.modByMonicHom 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

• q.modByMonicHom = { 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 : q.Monic) {x : S} (hx : (Polynomial.aeval x) q = 0) : (Polynomial.aeval x) (p %ₘ q) = (Polynomial.aeval x) p

instance Polynomial.instNoZeroDivisors {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) : (p * q).natDegree = p.natDegree + q.natDegree

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

@[simp]

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

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

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) : p.natDegree ≤ q.natDegree

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) : p.degree ≤ q.degree

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₂ : q.degree < p.degree) : 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₂ : q.natDegree < p.natDegree) : 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 : q.degree < p.degree) : ¬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 : q.natDegree < p.natDegree) : ¬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₁) : ↑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} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} (h : IsUnit p) : p.natDegree = 0

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

@[simp]

theorem Polynomial.degree_coe_units {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) : (↑u).degree = 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 < p.degree) : ¬IsUnit p

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

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

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

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

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

theorem Polynomial.root_mul {R : Type u} {a : R} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} : (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot 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 : (p * q).IsRoot a) : p.IsRoot a ∨ q.IsRoot a

instance Polynomial.instIsDomain {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 : p.Monic) {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 : p.Monic) : 0 < a.degree

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 : p.Monic) : 0 < a.natDegree

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

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

theorem Polynomial.eq_zero_of_mul_eq_zero_of_smul {R : Type u} [CommSemiring R] (P : Polynomial R) (h : ∀ (r : R), r • P = 0 → r = 0) (Q : Polynomial R) : P * Q = 0 → Q = 0

theorem Polynomial.nmem_nonZeroDivisors_iff {R : Type u} [CommSemiring R] {P : Polynomial R} : P ∉ nonZeroDivisors (Polynomial R) ↔ ∃ (a : R), a ≠ 0 ∧ a • P = 0

McCoy theorem: a polynomial P : R[X] is a zerodivisor if and only if there is a : R such that a ≠ 0 and a • P = 0.

theorem Polynomial.mem_nonZeroDivisors_iff {R : Type u} [CommSemiring R] {P : Polynomial R} : P ∈ nonZeroDivisors (Polynomial R) ↔ ∀ (a : R), a • P = 0 → a = 0

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 ∣ p.comp (Polynomial.X + Polynomial.C t)

theorem Polynomial.comp_X_add_C_eq_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} (t : R) : p.comp (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) : p.comp (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 (p.comp (Polynomial.X + Polynomial.C t))

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

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

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) = (p.comp (Polynomial.X + Polynomial.C t)).trailingCoeff

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

theorem Polynomial.mem_nonZeroDivisors_of_leadingCoeff {R : Type u} [CommRing R] {p : Polynomial R} (h : p.leadingCoeff ∈ 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

@[simp]

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

theorem Polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [CommRing R] [IsDomain R] (u : (Polynomial R)ˣ) : (↑u).coeff 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) : p.degree = q.degree

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 : p.IsRoot x) : p.degree = 1

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

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 : p.degree ≠ 0) (a : R) : (p /ₘ (Polynomial.X - Polynomial.C a)).leadingCoeff = p.leadingCoeff

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₁ : q.natDegree ≤ p.natDegree) (h₂ : p.leadingCoeff = q.leadingCoeff) : 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₁ : q.natDegree ≤ p.natDegree) (h₂ : q.leadingCoeff ∣ p.leadingCoeff) : 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₁ : q.natDegree ≤ p.natDegree) : 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₁ : p.degree = q.degree) : 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 : 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} [CommRing R] {p : Polynomial R} {q : Polynomial R} (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} [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 : p.degree = 1) (hm : p.Monic) : 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 : p.degree = 1) (hm : p.Monic) : Irreducible p

@[simp]

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

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

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

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

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

theorem Polynomial.comp_eq_zero_iff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} : 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} [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.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) ≤ p.degree ∧ ∀ (a : R), Multiset.count a s = Polynomial.rootMultiplicity a 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 f.leadingCoeff) (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 : f.Monic) (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.