doc-next-gen

Mathlib.Algebra.Polynomial.RingDivision

Module docstring

{"# Theory of univariate polynomials

We prove basic results about univariate polynomials.

"}

Polynomial.natDegree_pos_of_aeval_root theorem
[Algebra R S] {p : R[X]} (hp : p ≠ 0) {z : S} (hz : aeval z p = 0) (inj : ∀ x : R, algebraMap R S x = 0 → x = 0) : 0 < p.natDegree
Full source 
theorem natDegree_pos_of_aeval_root [Algebra R S] {p : R[X]} (hp : p ≠ 0) {z : S}
    (hz : aeval z p = 0) (inj : ∀ x : R, algebraMap R S x = 0 → x = 0) : 0 < p.natDegree :=
  natDegree_pos_of_eval₂_root hp (algebraMap R S) hz inj
Nonzero Polynomials with Roots Have Positive Degree
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra. For any nonzero polynomial $p \in R[X]$ and any element $z \in S$ such that $p(z) = 0$ (where $p(z)$ is the evaluation of $p$ at $z$ via the algebra homomorphism), and assuming the algebra map $R \to S$ is injective, the natural degree of $p$ is positive, i.e., $\text{natDegree}(p) > 0$.
Polynomial.degree_pos_of_aeval_root theorem
[Algebra R S] {p : R[X]} (hp : p ≠ 0) {z : S} (hz : aeval z p = 0) (inj : ∀ x : R, algebraMap R S x = 0 → x = 0) : 0 < p.degree
Full source 
theorem degree_pos_of_aeval_root [Algebra R S] {p : R[X]} (hp : p ≠ 0) {z : S} (hz : aeval z p = 0)
    (inj : ∀ x : R, algebraMap R S x = 0 → x = 0) : 0 < p.degree :=
  natDegree_pos_iff_degree_pos.mp (natDegree_pos_of_aeval_root hp hz inj)
Nonzero Polynomials with Roots Have Positive Degree
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra. For any nonzero polynomial $p \in R[X]$ and any element $z \in S$ such that $p(z) = 0$ (where evaluation is via the algebra homomorphism), and assuming the algebra map $R \to S$ is injective, the degree of $p$ is positive, i.e., $\deg(p) > 0$.
Polynomial.smul_modByMonic theorem
(c : R) (p : R[X]) : c • p %ₘ q = c • (p %ₘ q)
Full source 
theorem smul_modByMonic (c : R) (p : R[X]) : c • p %ₘ q = c • (p %ₘ q) := by
  by_cases hq : q.Monic
  · rcases subsingleton_or_nontrivial R with hR | hR
    · simp only [eq_iff_true_of_subsingleton]
    · exact
      (div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
          ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div p hq],
            (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2
  · simp_rw [modByMonic_eq_of_not_monic _ hq]
Scalar Multiplication Commutes with Remainder in Polynomial Division by Monic Polynomial
Informal description
For any scalar $c \in R$ and any polynomial $p \in R[X]$, the remainder of the scalar multiple $c \cdot p$ divided by a monic polynomial $q$ is equal to the scalar multiple of the remainder of $p$ divided by $q$, i.e., $$ (c \cdot p) \mod q = c \cdot (p \mod q). $$
Polynomial.modByMonicHom definition
(q : R[X]) : R[X] →ₗ[R] R[X]
Full source 
/-- `_ %ₘ q` as an `R`-linear map. -/
@[simps]
def modByMonicHom (q : R[X]) : R[X]R[X] →ₗ[R] R[X] where
  toFun p := p %ₘ q
  map_add' := add_modByMonic
  map_smul' := smul_modByMonic
Linear map of polynomial remainder modulo q
Informal description
The linear map $R[X] \to R[X]$ that sends a polynomial $p$ to its remainder $p \mod q$ when divided by a fixed polynomial $q$. This map is $R$-linear, meaning it satisfies: 1. Additivity: $(p_1 + p_2) \mod q = (p_1 \mod q) + (p_2 \mod q)$ 2. Homogeneity: $(c \cdot p) \mod q = c \cdot (p \mod q)$ for any scalar $c \in R$
Polynomial.mem_ker_modByMonic theorem
(hq : q.Monic) {p : R[X]} : p ∈ LinearMap.ker (modByMonicHom q) ↔ q ∣ p
Full source 
theorem mem_ker_modByMonic (hq : q.Monic) {p : R[X]} :
    p ∈ LinearMap.ker (modByMonicHom q)p ∈ LinearMap.ker (modByMonicHom q) ↔ q ∣ p :=
  LinearMap.mem_ker.trans (modByMonic_eq_zero_iff_dvd hq)
Kernel Membership in Remainder Map Characterizes Divisibility by Monic Polynomial
Informal description
For any monic polynomial $q$ over a commutative ring $R$ and any polynomial $p$ over $R$, the polynomial $p$ belongs to the kernel of the remainder map modulo $q$ if and only if $q$ divides $p$, i.e., \[ p \in \ker(\text{modByMonicHom } q) \leftrightarrow q \mid p. \]
Polynomial.aeval_modByMonic_eq_self_of_root theorem
[Algebra R S] {p q : R[X]} (hq : q.Monic) {x : S} (hx : aeval x q = 0) : aeval x (p %ₘ q) = aeval x p
Full source 
theorem aeval_modByMonic_eq_self_of_root [Algebra R S] {p q : R[X]} (hq : q.Monic) {x : S}
    (hx : aeval x q = 0) : aeval x (p %ₘ q) = aeval x p := by
    --`eval₂_modByMonic_eq_self_of_root` doesn't work here as it needs commutativity
  rw [modByMonic_eq_sub_mul_div p hq, map_sub, map_mul, hx, zero_mul,
    sub_zero]
Evaluation of Polynomial Modulo Monic Polynomial at Root
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra. For any monic polynomial $q \in R[X]$ and any polynomial $p \in R[X]$, if $x \in S$ is a root of $q$ (i.e., $\text{aeval}_x(q) = 0$), then evaluating $p$ modulo $q$ at $x$ is equal to evaluating $p$ at $x$: \[ \text{aeval}_x(p \mod q) = \text{aeval}_x(p). \]
Polynomial.trailingDegree_mul theorem
: (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
Full source 
theorem trailingDegree_mul : (p * q).trailingDegree = p.trailingDegree + q.trailingDegree := by
  by_cases hp : p = 0
  · rw [hp, zero_mul, trailingDegree_zero, top_add]
  by_cases hq : q = 0
  · rw [hq, mul_zero, trailingDegree_zero, add_top]
  · rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
    trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]
    apply WithTop.coe_add
Trailing Degree is Additive under Polynomial Multiplication
Informal description
For any two polynomials $p$ and $q$ over a semiring $R$, the trailing degree of their product $p \cdot q$ is equal to the sum of their individual trailing degrees, i.e., $\text{trailingDegree}(p \cdot q) = \text{trailingDegree}(p) + \text{trailingDegree}(q)$.
Polynomial.rootMultiplicity_eq_rootMultiplicity theorem
{p : R[X]} {t : R} : p.rootMultiplicity t = (p.comp (X + C t)).rootMultiplicity 0
Full source 
theorem rootMultiplicity_eq_rootMultiplicity {p : R[X]} {t : R} :
    p.rootMultiplicity t = (p.comp (X + C t)).rootMultiplicity 0 := by
  classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]
Root Multiplicity Invariance under Translation: $\text{rootMultiplicity}(p, t) = \text{rootMultiplicity}(p(X + t), 0)$
Informal description
For any polynomial $p \in R[X]$ and any element $t \in R$, the root multiplicity of $t$ in $p$ is equal to the root multiplicity of $0$ in the composition $p(X + t)$. That is, \[ \text{rootMultiplicity}(p, t) = \text{rootMultiplicity}(p(X + t), 0). \]
Polynomial.rootMultiplicity_eq_natTrailingDegree theorem
{p : R[X]} {t : R} : p.rootMultiplicity t = (p.comp (X + C t)).natTrailingDegree
Full source 
/-- See `Polynomial.rootMultiplicity_eq_natTrailingDegree'` for the special case of `t = 0`. -/
theorem rootMultiplicity_eq_natTrailingDegree {p : R[X]} {t : R} :
    p.rootMultiplicity t = (p.comp (X + C t)).natTrailingDegree :=
  rootMultiplicity_eq_rootMultiplicity.trans rootMultiplicity_eq_natTrailingDegree'
Root Multiplicity Equals Natural Trailing Degree under Translation: $\text{rootMultiplicity}(p, t) = \text{natTrailingDegree}(p(X + t))$
Informal description
For any polynomial $p \in R[X]$ over a commutative ring $R$ and any element $t \in R$, the root multiplicity of $t$ in $p$ is equal to the natural trailing degree of the polynomial $p(X + t)$. That is, \[ \text{rootMultiplicity}(p, t) = \text{natTrailingDegree}(p(X + t)). \]
Polynomial.mem_nonZeroDivisors_of_leadingCoeff theorem
{p : R[X]} (h : p.leadingCoeff ∈ R⁰) : p ∈ R[X]⁰
Full source 
theorem mem_nonZeroDivisors_of_leadingCoeff {p : R[X]} (h : p.leadingCoeff ∈ R⁰) : p ∈ R[X]⁰ :=
  mem_nonzeroDivisors_of_coeff_mem _ h
Non-zero-divisor leading coefficient implies polynomial is a non-zero-divisor
Informal description
Let $R$ be a commutative semiring and $R[X]$ the polynomial ring over $R$. For any polynomial $p \in R[X]$, if the leading coefficient of $p$ is a non-zero-divisor in $R$, then $p$ is a non-zero-divisor in $R[X]$.
Polynomial.mem_nonZeroDivisors_of_trailingCoeff theorem
{p : R[X]} (h : p.trailingCoeff ∈ R⁰) : p ∈ R[X]⁰
Full source 
theorem mem_nonZeroDivisors_of_trailingCoeff {p : R[X]} (h : p.trailingCoeff ∈ R⁰) : p ∈ R[X]⁰ :=
  mem_nonzeroDivisors_of_coeff_mem _ h
Polynomials with non-zero-divisor trailing coefficients are non-zero-divisors
Informal description
Let $R$ be a commutative semiring and $R[X]$ the polynomial ring over $R$. For any polynomial $p \in R[X]$, if the trailing coefficient of $p$ is a non-zero-divisor in $R$, then $p$ is a non-zero-divisor in $R[X]$.
Polynomial.natDegree_pos_of_monic_of_aeval_eq_zero theorem
[Nontrivial R] [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : R[X]} (hp : p.Monic) {x : S} (hx : aeval x p = 0) : 0 < p.natDegree
Full source 
theorem natDegree_pos_of_monic_of_aeval_eq_zero [Nontrivial R] [Semiring S] [Algebra R S]
    [FaithfulSMul R S] {p : R[X]} (hp : p.Monic) {x : S} (hx : aeval x p = 0) :
    0 < p.natDegree :=
  natDegree_pos_of_aeval_root (Monic.ne_zero hp) hx
    ((injective_iff_map_eq_zero (algebraMap R S)).mp (FaithfulSMul.algebraMap_injective R S))
Monic Polynomials with Roots Have Positive Degree
Informal description
Let $R$ be a nontrivial commutative ring and $S$ a semiring with an $R$-algebra structure such that the scalar multiplication action of $R$ on $S$ is faithful. For any monic polynomial $p \in R[X]$ and any element $x \in S$ such that the evaluation of $p$ at $x$ is zero (i.e., $p(x) = 0$), the natural degree of $p$ is positive, i.e., $\text{natDegree}(p) > 0$.
Polynomial.rootMultiplicity_mul_X_sub_C_pow theorem
{p : R[X]} {a : R} {n : ℕ} (h : p ≠ 0) : (p * (X - C a) ^ n).rootMultiplicity a = p.rootMultiplicity a + n
Full source 
theorem rootMultiplicity_mul_X_sub_C_pow {p : R[X]} {a : R} {n : ℕ} (h : p ≠ 0) :
    (p * (X - C a) ^ n).rootMultiplicity a = p.rootMultiplicity a + n := by
  have h2 := monic_X_sub_C a |>.pow n |>.mul_left_ne_zero h
  refine le_antisymm ?_ ?_
  · rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
      dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]
    exact pow_rootMultiplicity_not_dvd h a
  · rw [le_rootMultiplicity_iff h2, pow_add]
    exact mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _
Root Multiplicity of Product with Power of Linear Factor: $\text{rootMultiplicity}(a, p \cdot (X - a)^n) = \text{rootMultiplicity}(a, p) + n$
Informal description
For any nonzero polynomial $p$ over a commutative ring $R$, any element $a \in R$, and any natural number $n$, the root multiplicity of $a$ in the polynomial $p \cdot (X - a)^n$ is equal to the sum of the root multiplicity of $a$ in $p$ and $n$, i.e., \[ \text{rootMultiplicity}(a, p \cdot (X - a)^n) = \text{rootMultiplicity}(a, p) + n. \]
Polynomial.rootMultiplicity_X_sub_C_pow theorem
[Nontrivial R] (a : R) (n : ℕ) : rootMultiplicity a ((X - C a) ^ n) = n
Full source 
/-- The multiplicity of `a` as root of `(X - a) ^ n` is `n`. -/
theorem rootMultiplicity_X_sub_C_pow [Nontrivial R] (a : R) (n : ℕ) :
    rootMultiplicity a ((X - C a) ^ n) = n := by
  have := rootMultiplicity_mul_X_sub_C_pow (a := a) (n := n) C.map_one_ne_zero
  rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this
Root multiplicity of $(X - a)^n$ at $a$ is $n$
Informal description
Let $R$ be a nontrivial commutative ring. For any element $a \in R$ and natural number $n$, the root multiplicity of $a$ in the polynomial $(X - a)^n$ is equal to $n$.
Polynomial.rootMultiplicity_X_sub_C_self theorem
[Nontrivial R] {x : R} : rootMultiplicity x (X - C x) = 1
Full source 
theorem rootMultiplicity_X_sub_C_self [Nontrivial R] {x : R} :
    rootMultiplicity x (X - C x) = 1 :=
  pow_one (X - C x) ▸ rootMultiplicity_X_sub_C_pow x 1
Root multiplicity of $X - x$ at $x$ is 1
Informal description
Let $R$ be a nontrivial commutative ring. For any element $x \in R$, the root multiplicity of $x$ in the linear polynomial $X - x$ is equal to 1.
Polynomial.rootMultiplicity_X_sub_C theorem
[Nontrivial R] [DecidableEq R] {x y : R} : rootMultiplicity x (X - C y) = if x = y then 1 else 0
Full source 
theorem rootMultiplicity_X_sub_C [Nontrivial R] [DecidableEq R] {x y : R} :
    rootMultiplicity x (X - C y) = if x = y then 1 else 0 := by
  split_ifs with hxy
  · rw [hxy]
    exact rootMultiplicity_X_sub_C_self
  exact rootMultiplicity_eq_zero (mt root_X_sub_C.mp (Ne.symm hxy))
Root multiplicity of $X - y$ at $x$ is $1$ when $x = y$ and $0$ otherwise
Informal description
Let $R$ be a nontrivial commutative ring with decidable equality. For any elements $x, y \in R$, the root multiplicity of $x$ in the polynomial $X - y$ is $1$ if $x = y$ and $0$ otherwise. In other words: \[ \text{rootMultiplicity}(x, X - y) = \begin{cases} 1 & \text{if } x = y, \\ 0 & \text{otherwise.} \end{cases} \]
Polynomial.rootMultiplicity_mul' theorem
{p q : R[X]} {x : R} (hpq : (p /ₘ (X - C x) ^ p.rootMultiplicity x).eval x * (q /ₘ (X - C x) ^ q.rootMultiplicity x).eval x ≠ 0) : rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Full source 
theorem rootMultiplicity_mul' {p q : R[X]} {x : R}
    (hpq : (p /ₘ (X - C x) ^ p.rootMultiplicity x).eval x *
      (q /ₘ (X - C x) ^ q.rootMultiplicity x).eval x ≠ 0) :
    rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q := by
  simp_rw [eval_divByMonic_eq_trailingCoeff_comp] at hpq
  simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]
Additivity of Root Multiplicity in Polynomial Multiplication
Informal description
Let $R$ be a commutative ring and let $p, q \in R[X]$ be polynomials. For any $x \in R$, if the product of the evaluations of the reduced polynomials $\frac{p}{(X - x)^{n}}$ and $\frac{q}{(X - x)^{m}}$ at $x$ is nonzero (where $n$ and $m$ are the root multiplicities of $x$ in $p$ and $q$ respectively), then the root multiplicity of $x$ in the product $p \cdot q$ is the sum of the root multiplicities, i.e., \[ \text{rootMultiplicity}(x, p \cdot q) = \text{rootMultiplicity}(x, p) + \text{rootMultiplicity}(x, q). \]
Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X theorem
{p : R[X]} (hp : p.Monic) : ((-1) ^ p.natDegree * p.comp (-X)).Monic
Full source 
theorem Monic.neg_one_pow_natDegree_mul_comp_neg_X {p : R[X]} (hp : p.Monic) :
    ((-1) ^ p.natDegree * p.comp (-X)).Monic := by
  simp only [Monic]
  calc
    ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
        (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]
Monicity of $(-1)^{\deg p} \cdot p(-X)$ for monic polynomials $p$
Informal description
Let $R$ be a commutative ring and let $p \in R[X]$ be a monic polynomial. Then the polynomial $(-1)^{\deg p} \cdot p(-X)$ is also monic, where $\deg p$ denotes the degree of $p$ and $p(-X)$ is the composition of $p$ with $-X$.
Polynomial.degree_eq_degree_of_associated theorem
(h : Associated p q) : degree p = degree q
Full source 
theorem degree_eq_degree_of_associated (h : Associated p q) : degree p = degree q := by
  let ⟨u, hu⟩ := h
  simp [hu.symm]
Degree Preservation under Polynomial Association
Informal description
Let $R$ be a commutative ring and let $p, q \in R[X]$ be univariate polynomials. If $p$ and $q$ are associated (i.e., there exists a unit $u \in R[X]$ such that $p \cdot u = q$), then their degrees are equal: $\deg(p) = \deg(q)$.
Polynomial.prime_X theorem
: Prime (X : R[X])
Full source 
theorem prime_X : Prime (X : R[X]) := by
  convert prime_X_sub_C (0 : R)
  simp
Primality of the Polynomial Variable $X$ in $R[X]$
Informal description
The polynomial variable $X$ in the polynomial ring $R[X]$ is a prime element.
Polynomial.Monic.prime_of_degree_eq_one theorem
(hp1 : degree p = 1) (hm : Monic p) : Prime p
Full source 
theorem Monic.prime_of_degree_eq_one (hp1 : degree p = 1) (hm : Monic p) : Prime p :=
  have : p = X - C (-p.coeff 0) := by simpa [hm.leadingCoeff] using eq_X_add_C_of_degree_eq_one hp1
  this.symm ▸ prime_X_sub_C _
Monic Linear Polynomials are Prime in $R[X]$
Informal description
Let $p$ be a monic polynomial over a commutative ring $R$ with degree equal to 1. Then $p$ is a prime element in the polynomial ring $R[X]$.
Polynomial.irreducible_X_sub_C theorem
(r : R) : Irreducible (X - C r)
Full source 
theorem irreducible_X_sub_C (r : R) : Irreducible (X - C r) :=
  (prime_X_sub_C r).irreducible
Irreducibility of Linear Polynomials: $X - r$ is Irreducible in $R[X]$
Informal description
For any element $r$ in a commutative ring $R$, the linear polynomial $X - r$ is irreducible in the polynomial ring $R[X]$. That is, it cannot be factored into a product of two non-constant polynomials.
Polynomial.irreducible_X theorem
: Irreducible (X : R[X])
Full source 
theorem irreducible_X : Irreducible (X : R[X]) :=
  Prime.irreducible prime_X
Irreducibility of the Polynomial Variable $X$ in $R[X]$
Informal description
The polynomial variable $X$ in the polynomial ring $R[X]$ is irreducible. That is, $X$ cannot be factored into a product of two non-constant polynomials over the commutative ring $R$.
Polynomial.Monic.irreducible_of_degree_eq_one theorem
(hp1 : degree p = 1) (hm : Monic p) : Irreducible p
Full source 
theorem Monic.irreducible_of_degree_eq_one (hp1 : degree p = 1) (hm : Monic p) : Irreducible p :=
  (hm.prime_of_degree_eq_one hp1).irreducible
Irreducibility of monic linear polynomials in $R[X]$
Informal description
Let $R$ be a commutative ring and $p \in R[X]$ be a monic polynomial of degree 1. Then $p$ is irreducible in $R[X]$.
Polynomial.aeval_ne_zero_of_isCoprime theorem
{R} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S] {p q : R[X]} (h : IsCoprime p q) (s : S) : aeval s p ≠ 0 ∨ aeval s q ≠ 0
Full source 
lemma aeval_ne_zero_of_isCoprime {R} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S]
    {p q : R[X]} (h : IsCoprime p q) (s : S) : aevalaeval s p ≠ 0aeval s p ≠ 0 ∨ aeval s q ≠ 0 := by
  by_contra! hpq
  rcases h with ⟨_, _, h⟩
  apply_fun aeval s at h
  simp only [map_add, map_mul, map_one, hpq.left, hpq.right, mul_zero, add_zero, zero_ne_one] at h
Nonzero Evaluation of Coprime Polynomials in Nontrivial Algebras
Informal description
Let $R$ be a commutative semiring and $S$ a nontrivial semiring with an $R$-algebra structure. For any two coprime polynomials $p, q \in R[X]$ and any element $s \in S$, at least one of the evaluations $\text{aeval}_s(p)$ or $\text{aeval}_s(q)$ is nonzero.
Polynomial.isCoprime_X_sub_C_of_isUnit_sub theorem
{R} [CommRing R] {a b : R} (h : IsUnit (a - b)) : IsCoprime (X - C a) (X - C b)
Full source 
theorem isCoprime_X_sub_C_of_isUnit_sub {R} [CommRing R] {a b : R} (h : IsUnit (a - b)) :
    IsCoprime (X - C a) (X - C b) :=
  ⟨-C h.unit⁻¹.val, C h.unit⁻¹.val, by
    rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]
    rw [← C_1]
    congr
    exact h.val_inv_mul⟩
Coprimality of $X - a$ and $X - b$ when $a - b$ is a unit
Informal description
Let $R$ be a commutative ring, and let $a, b \in R$ be elements such that $a - b$ is a unit in $R$. Then the polynomials $X - a$ and $X - b$ in $R[X]$ are coprime, i.e., there exist polynomials $p, q \in R[X]$ such that $p(X)(X - a) + q(X)(X - b) = 1$.
Polynomial.pairwise_coprime_X_sub_C theorem
{K} [Field K] {I : Type v} {s : I → K} (H : Function.Injective s) : Pairwise (IsCoprime on fun i : I => X - C (s i))
Full source 
theorem pairwise_coprime_X_sub_C {K} [Field K] {I : Type v} {s : I → K} (H : Function.Injective s) :
    Pairwise (IsCoprimeIsCoprime on fun i : I => X - C (s i)) := fun _ _ hij =>
  isCoprime_X_sub_C_of_isUnit_sub (sub_ne_zero_of_ne <| H.ne hij).isUnit
Pairwise Coprimality of Linear Polynomials over a Field
Informal description
Let $K$ be a field, $I$ a type, and $s \colon I \to K$ an injective function. Then the family of polynomials $\{X - s(i)\}_{i \in I}$ is pairwise coprime, meaning that for any two distinct indices $i, j \in I$, the polynomials $X - s(i)$ and $X - s(j)$ are coprime in $K[X]$.
Polynomial.rootMultiplicity_mul theorem
{p q : R[X]} {x : R} (hpq : p * q ≠ 0) : rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Full source 
theorem rootMultiplicity_mul {p q : R[X]} {x : R} (hpq : p * q ≠ 0) :
    rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q := by
  classical
  have hp : p ≠ 0 := left_ne_zero_of_mul hpq
  have hq : q ≠ 0 := right_ne_zero_of_mul hpq
  rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
Additivity of Root Multiplicity in Polynomial Multiplication: $\text{rootMultiplicity}(x, p \cdot q) = \text{rootMultiplicity}(x, p) + \text{rootMultiplicity}(x, q)$
Informal description
For any nonzero polynomials $p$ and $q$ in $R[X]$ and any element $x \in R$, the root multiplicity of $x$ in the product $p \cdot q$ is equal to the sum of the root multiplicities of $x$ in $p$ and $x$ in $q$, i.e., \[ \text{rootMultiplicity}(x, p \cdot q) = \text{rootMultiplicity}(x, p) + \text{rootMultiplicity}(x, q). \]
Polynomial.exists_multiset_roots theorem
[DecidableEq R] : ∀ {p : R[X]} (_ : p ≠ 0), ∃ s : Multiset R, (Multiset.card s : WithBot ℕ) ≤ degree p ∧ ∀ a, s.count a = rootMultiplicity a p
Full source 
theorem exists_multiset_roots [DecidableEq R] :
    ∀ {p : R[X]} (_ : p ≠ 0), ∃ s : Multiset R,
      (Multiset.card s : WithBot ℕ) ≤ degree p ∧ ∀ a, s.count a = rootMultiplicity a p
  | p, hp =>
    haveI := Classical.propDecidable (∃ x, IsRoot p x)
    if h : ∃ x, IsRoot p x then
      let ⟨x, hx⟩ := h
      have hpd : 0 < degree p := degree_pos_of_root hp hx
      have hd0 : p /ₘ (X - C x) ≠ 0 := fun h => by
        rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp; exact hp rfl
      have wf : degree (p /ₘ (X - C x)) < degree p :=
        degree_divByMonic_lt _ (monic_X_sub_C x) hp ((degree_X_sub_C x).symm ▸ by decide)
      let ⟨t, htd, htr⟩ := @exists_multiset_roots _ (p /ₘ (X - C x)) hd0
      have hdeg : degree (X - C x) ≤ degree p := by
        rw [degree_X_sub_C, degree_eq_natDegree hp]
        rw [degree_eq_natDegree hp] at hpd
        exact WithBot.coe_le_coe.2 (WithBot.coe_lt_coe.1 hpd)
      have hdiv0 : p /ₘ (X - C x) ≠ 0 :=
        mt (divByMonic_eq_zero_iff (monic_X_sub_C x)).1 <| not_lt.2 hdeg
      ⟨x ::ₘ t,
        calc
          (card (x ::ₘ t) : WithBot ℕ) = Multiset.card t + 1 := by
            congr
            exact mod_cast Multiset.card_cons _ _
          _ ≤ degree p := by
            rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm]
            exact add_le_add (le_refl (1 : WithBot ℕ)) htd,
        by
          intro a
          conv_rhs => rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]
          rw [rootMultiplicity_mul (mul_ne_zero (X_sub_C_ne_zero x) hdiv0),
            rootMultiplicity_X_sub_C, ← htr a]
          split_ifs with ha
          · rw [ha, count_cons_self, add_comm]
          · rw [count_cons_of_ne ha, zero_add]⟩
    else
      ⟨0, (degree_eq_natDegree hp).symm ▸ WithBot.coe_le_coe.2 (Nat.zero_le _), by
        intro a
        rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]⟩
termination_by p => natDegree p
decreasing_by {
  simp_wf
  apply (Nat.cast_lt (α := WithBot ℕ)).mp
  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
  assumption}
Existence of Root Multiset for Nonzero Polynomials
Informal description
For any nonzero polynomial $p$ over a commutative ring $R$ with decidable equality, there exists a multiset $s$ of roots of $p$ such that: 1. The cardinality of $s$ (counted with multiplicity) is at most the degree of $p$. 2. For every element $a \in R$, the multiplicity of $a$ in $s$ equals the root multiplicity of $a$ in $p$.