Mathlib.Algebra.Polynomial.FieldDivision

Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero theorem

(p : R[X]) (t : R) (hnezero : derivative p ≠ 0) : p.rootMultiplicity t - 1 ≤ p.derivative.rootMultiplicity t

Full source

theorem rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero
    (p : R[X]) (t : R) (hnezero : derivativederivative p ≠ 0) :
    p.rootMultiplicity t - 1 ≤ p.derivative.rootMultiplicity t :=
  (le_rootMultiplicity_iff hnezero).2 <|
    pow_sub_one_dvd_derivative_of_pow_dvd (p.pow_rootMultiplicity_dvd t)

Inequality Relating Root Multiplicities of a Polynomial and Its Derivative

Informal description

For any polynomial $p$ over a commutative ring $R$ and any element $t \in R$, if the derivative $p'$ is nonzero, then the root multiplicity of $t$ in $p$ minus one is less than or equal to the root multiplicity of $t$ in $p'$. In other words, \[ \text{rootMultiplicity}(t, p) - 1 \leq \text{rootMultiplicity}(t, p'). \]

Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors theorem

 {p : R[X]} {t : R} (hpt : Polynomial.IsRoot p t) (hnzd : (p.rootMultiplicity t : R) ∈ nonZeroDivisors R) :
  (derivative p).rootMultiplicity t = p.rootMultiplicity t - 1

Full source

theorem derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors
    {p : R[X]} {t : R} (hpt : Polynomial.IsRoot p t)
    (hnzd : (p.rootMultiplicity t : R) ∈ nonZeroDivisors R) :
    (derivative p).rootMultiplicity t = p.rootMultiplicity t - 1 := by
  by_cases h : p = 0
  · simp only [h, map_zero, rootMultiplicity_zero]
  obtain ⟨g, hp, hndvd⟩ := p.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h t
  set m := p.rootMultiplicity t
  have hm : m - 1 + 1 = m := Nat.sub_add_cancel <| (rootMultiplicity_pos h).2 hpt
  have hndvd : ¬(X - C t) ^ m ∣ derivative p := by
    rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _),
      derivative_X_sub_C_pow, ← hm, pow_succ, hm, mul_comm (C _), mul_assoc,
      dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]
    rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢
    rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
  have hnezero : derivativederivative p ≠ 0 := fun h ↦ hndvd (by rw [h]; exact dvd_zero _)
  exact le_antisymm (by rwa [rootMultiplicity_le_iff hnezero, hm])
    (rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero _ t hnezero)

Root Multiplicity of Derivative: $\text{rootMultiplicity}(t, p') = n-1$ when $n$ is a non-zero-divisor

Informal description

Let $R$ be a commutative ring and $p \in R[X]$ be a polynomial with a root at $t \in R$. If the root multiplicity $n$ of $t$ in $p$ is a non-zero-divisor in $R$, then the root multiplicity of $t$ in the derivative $p'$ is exactly $n-1$. In other words: \[ \text{rootMultiplicity}(t, p') = \text{rootMultiplicity}(t, p) - 1. \]

Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity theorem

{p : R[X]} {t : R} {n : ℕ} (hn : n < p.rootMultiplicity t) : (derivative^[n] p).IsRoot t

Full source

theorem isRoot_iterate_derivative_of_lt_rootMultiplicity {p : R[X]} {t : R} {n : ℕ}
    (hn : n < p.rootMultiplicity t) : (derivativederivative^[n] p).IsRoot t :=
  dvd_iff_isRoot.mp <| (dvd_pow_self _ <| Nat.sub_ne_zero_of_lt hn).trans
    (pow_sub_dvd_iterate_derivative_of_pow_dvd _ <| p.pow_rootMultiplicity_dvd t)

Roots of Iterated Derivatives Below Root Multiplicity: $(\partial^n p)(t) = 0$ for $n < \text{rootMultiplicity}(p, t)$

Informal description

For any polynomial $p \in R[X]$ and any element $t \in R$, if $n$ is a natural number such that $n < \text{rootMultiplicity}(p, t)$, then $t$ is a root of the $n$-th iterate of the derivative of $p$, i.e., $(\partial^n p)(t) = 0$.

Polynomial.eval_iterate_derivative_rootMultiplicity theorem

 {p : R[X]} {t : R} :
  (derivative^[p.rootMultiplicity t] p).eval t =
    (p.rootMultiplicity t).factorial • (p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t

Full source

theorem eval_iterate_derivative_rootMultiplicity {p : R[X]} {t : R} :
    (derivativederivative^[p.rootMultiplicity t] p).eval t =
      (p.rootMultiplicity t).factorial • (p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t := by
  set m := p.rootMultiplicity t with hm
  conv_lhs => rw [← p.pow_mul_divByMonic_rootMultiplicity_eq t, ← hm]
  rw [iterate_derivative_mul, eval_finset_sum, sum_eq_single_of_mem _ (mem_range.mpr m.succ_pos)]
  · rw [m.choose_zero_right, one_smul, eval_mul, m.sub_zero, iterate_derivative_X_sub_pow_self,
      eval_natCast, nsmul_eq_mul]; rfl
  · intro b hb hb0
    rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]

Evaluation of Iterated Derivative at Root: $\frac{d^n p}{dX^n}(t) = n! \cdot \left(\frac{p}{(X-t)^n}\right)(t)$

Informal description

For any polynomial $p$ over a commutative ring $R$ and any element $t \in R$, evaluating the $n$-th iterate of the derivative of $p$ at $t$ (where $n$ is the root multiplicity of $t$ in $p$) gives $n!$ times the evaluation at $t$ of the quotient polynomial $p$ divided by $(X - t)^n$. That is, \[ \left(\frac{d^n p}{dX^n}\right)(t) = n! \cdot \left(\frac{p}{(X - t)^n}\right)(t) \] where $n = \text{rootMultiplicity}(t, p)$.

Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors theorem

 {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t)
  (hnzd : (n.factorial : R) ∈ nonZeroDivisors R) : n < p.rootMultiplicity t

Full source

theorem lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors
    {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hroot : ∀ m ≤ n, (derivativederivative^[m] p).IsRoot t)
    (hnzd : (n.factorial : R) ∈ nonZeroDivisors R) :
    n < p.rootMultiplicity t := by
  by_contra! h'
  replace hroot := hroot _ h'
  simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot
  obtain ⟨q, hq⟩ := Nat.cast_dvd_cast (α := R) <| Nat.factorial_dvd_factorial h'
  rw [hq, mul_mem_nonZeroDivisors] at hnzd
  rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot
  exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

Lower Bound on Root Multiplicity via Vanishing Derivatives and Non-zero-divisor Condition

Informal description

Let $p \in R[X]$ be a nonzero polynomial over a commutative ring $R$, let $t \in R$, and let $n \in \mathbb{N}$. If: 1. For all $m \leq n$, the $m$-th iterate of the derivative of $p$ evaluated at $t$ is zero (i.e., $(\partial^m p)(t) = 0$ for all $m \leq n$), and 2. The factorial $n!$ is a non-zero-divisor in $R$ (i.e., $n! \in R^0$), then $n$ is strictly less than the root multiplicity of $t$ in $p$ (i.e., $n < \text{rootMultiplicity}(p, t)$).

Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' theorem

 {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t)
  (hnzd : ∀ m ≤ n, m ≠ 0 → (m : R) ∈ nonZeroDivisors R) : n < p.rootMultiplicity t

Full source

theorem lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors'
    {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hroot : ∀ m ≤ n, (derivativederivative^[m] p).IsRoot t)
    (hnzd : ∀ m ≤ n, m ≠ 0 → (m : R) ∈ nonZeroDivisors R) :
    n < p.rootMultiplicity t := by
  apply lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot
  clear hroot
  induction n with
  | zero =>
    simp only [Nat.factorial_zero, Nat.cast_one]
    exact Submonoid.one_mem _
  | succ n ih =>
    rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
    exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

Lower Bound on Root Multiplicity via Vanishing Derivatives and Non-zero-divisor Condition (Stronger Version)

Informal description

Let $p \in R[X]$ be a nonzero polynomial over a commutative ring $R$, let $t \in R$, and let $n \in \mathbb{N}$. If: 1. For all $m \leq n$, the $m$-th iterate of the derivative of $p$ evaluated at $t$ is zero (i.e., $(\partial^m p)(t) = 0$ for all $m \leq n$), and 2. For all $0 < m \leq n$, the natural number $m$ is a non-zero-divisor in $R$ (i.e., $m \in R^0$), then $n$ is strictly less than the root multiplicity of $t$ in $p$ (i.e., $n < \text{rootMultiplicity}(p, t)$).

Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors theorem

 {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : (n.factorial : R) ∈ nonZeroDivisors R) :
  n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t

Full source

theorem lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors
    {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hnzd : (n.factorial : R) ∈ nonZeroDivisors R) :
    n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t :=
  ⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| hm.trans_lt hn,
    fun hr ↦ lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hr hnzd⟩

Characterization of Root Multiplicity via Vanishing Derivatives and Non-zero-divisor Condition

Informal description

Let $p \in R[X]$ be a nonzero polynomial over a commutative ring $R$, let $t \in R$, and let $n \in \mathbb{N}$. If the factorial $n!$ is a non-zero-divisor in $R$, then the following are equivalent: 1. $n$ is strictly less than the root multiplicity of $t$ in $p$ (i.e., $n < \text{rootMultiplicity}(p, t)$). 2. For all $m \leq n$, the $m$-th iterate of the derivative of $p$ evaluated at $t$ is zero (i.e., $(\partial^m p)(t) = 0$ for all $m \leq n$).

Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' theorem

 {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ∀ m ≤ n, m ≠ 0 → (m : R) ∈ nonZeroDivisors R) :
  n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t

Full source

theorem lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors'
    {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hnzd : ∀ m ≤ n, m ≠ 0 → (m : R) ∈ nonZeroDivisors R) :
    n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t :=
  ⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| Nat.lt_of_le_of_lt hm hn,
    fun hr ↦ lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' h hr hnzd⟩

Characterization of Root Multiplicity via Vanishing Derivatives and Non-zero-divisor Condition (Stronger Version)

Informal description

Let $p \in R[X]$ be a nonzero polynomial over a commutative ring $R$, let $t \in R$, and let $n \in \mathbb{N}$. If for all $0 < m \leq n$, the natural number $m$ is a non-zero-divisor in $R$, then the following are equivalent: 1. $n$ is strictly less than the root multiplicity of $t$ in $p$ (i.e., $n < \text{rootMultiplicity}(p, t)$). 2. For all $m \leq n$, the $m$-th iterate of the derivative of $p$ evaluated at $t$ is zero (i.e., $(\partial^m p)(t) = 0$ for all $m \leq n$).

Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative theorem

{p : R[X]} {t : R} (h : p ≠ 0) : 1 < p.rootMultiplicity t ↔ ∀ m ≤ 1, (derivative^[m] p).IsRoot t

Full source

theorem one_lt_rootMultiplicity_iff_isRoot_iterate_derivative
    {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ ∀ m ≤ 1, (derivative^[m] p).IsRoot t :=
  lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors h
    (by rw [Nat.factorial_one, Nat.cast_one]; exact Submonoid.one_mem _)

Characterization of Root Multiplicity Greater Than One via Vanishing Polynomial and Its Derivative

Informal description

For any nonzero polynomial $p \in R[X]$ over a commutative ring $R$ and any element $t \in R$, the following are equivalent: 1. The root multiplicity of $t$ in $p$ is greater than 1 (i.e., $\text{rootMultiplicity}(p, t) > 1$). 2. Both $p$ and its first derivative $\partial p$ vanish at $t$ (i.e., $p(t) = 0$ and $(\partial p)(t) = 0$).

Polynomial.one_lt_rootMultiplicity_iff_isRoot theorem

{p : R[X]} {t : R} (h : p ≠ 0) : 1 < p.rootMultiplicity t ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Full source

theorem one_lt_rootMultiplicity_iff_isRoot
    {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ p.IsRoot t ∧ (derivative p).IsRoot t := by
  rw [one_lt_rootMultiplicity_iff_isRoot_iterate_derivative h]
  refine ⟨fun h ↦ ⟨h 0 (by norm_num), h 1 (by norm_num)⟩, fun ⟨h0, h1⟩ m hm ↦ ?_⟩
  obtain (_|_|m) := m
  exacts [h0, h1, by omega]

Root Multiplicity Greater Than One if and only if Both Polynomial and Its Derivative Vanish at Point

Informal description

For any nonzero polynomial $p \in R[X]$ over a commutative ring $R$ and any element $t \in R$, the root multiplicity of $t$ in $p$ is greater than 1 if and only if both $p(t) = 0$ and $(\partial p)(t) = 0$, where $\partial p$ denotes the derivative of $p$.

Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd theorem

[GCDMonoid R[X]] {p : R[X]} {t : R} (h : p ≠ 0) : 1 < p.rootMultiplicity t ↔ (gcd p (derivative p)).IsRoot t

Full source

theorem one_lt_rootMultiplicity_iff_isRoot_gcd
    [GCDMonoid R[X]] {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ (gcd p (derivative p)).IsRoot t := by
  simp_rw [one_lt_rootMultiplicity_iff_isRoot h, ← dvd_iff_isRoot, dvd_gcd_iff]

Root Multiplicity Greater Than One via GCD of Polynomial and Its Derivative

Informal description

Let $R$ be a commutative ring such that the polynomial ring $R[X]$ is a GCD monoid. For any nonzero polynomial $p \in R[X]$ and any element $t \in R$, the root multiplicity of $t$ in $p$ is greater than 1 if and only if $t$ is a root of the greatest common divisor of $p$ and its derivative $\partial p$, i.e., $\gcd(p, \partial p)(t) = 0$.

Polynomial.derivative_rootMultiplicity_of_root theorem

[CharZero R] {p : R[X]} {t : R} (hpt : p.IsRoot t) : p.derivative.rootMultiplicity t = p.rootMultiplicity t - 1

Full source

theorem derivative_rootMultiplicity_of_root [CharZero R] {p : R[X]} {t : R} (hpt : p.IsRoot t) :
    p.derivative.rootMultiplicity t = p.rootMultiplicity t - 1 := by
  by_cases h : p = 0
  · rw [h, map_zero, rootMultiplicity_zero]
  exact derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors hpt <|
    mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 ((rootMultiplicity_pos h).2 hpt).ne'

Root multiplicity of derivative in characteristic zero: $\text{rootMultiplicity}(t, p') = n-1$

Informal description

Let $R$ be a commutative ring of characteristic zero, $p \in R[X]$ a polynomial, and $t \in R$ a root of $p$. Then the root multiplicity of $t$ in the derivative $p'$ equals the root multiplicity of $t$ in $p$ minus one, i.e., \[ \text{rootMultiplicity}(t, p') = \text{rootMultiplicity}(t, p) - 1. \]

Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity theorem

[CharZero R] (p : R[X]) (t : R) : p.rootMultiplicity t - 1 ≤ p.derivative.rootMultiplicity t

Full source

theorem rootMultiplicity_sub_one_le_derivative_rootMultiplicity [CharZero R] (p : R[X]) (t : R) :
    p.rootMultiplicity t - 1 ≤ p.derivative.rootMultiplicity t := by
  by_cases h : p.IsRoot t
  · exact (derivative_rootMultiplicity_of_root h).symm.le
  · rw [rootMultiplicity_eq_zero h, zero_tsub]
    exact zero_le _

Lower bound on derivative's root multiplicity: $\text{rootMultiplicity}(t, p) - 1 \leq \text{rootMultiplicity}(t, p')$ in characteristic zero

Informal description

Let $R$ be a commutative ring of characteristic zero, $p \in R[X]$ a polynomial, and $t \in R$. Then the root multiplicity of $t$ in $p$ minus one is less than or equal to the root multiplicity of $t$ in the derivative $p'$, i.e., \[ \text{rootMultiplicity}(t, p) - 1 \leq \text{rootMultiplicity}(t, p'). \]

Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative theorem

 [CharZero R] {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t) :
  n < p.rootMultiplicity t

Full source

theorem lt_rootMultiplicity_of_isRoot_iterate_derivative
    [CharZero R] {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hroot : ∀ m ≤ n, (derivativederivative^[m] p).IsRoot t) :
    n < p.rootMultiplicity t :=
  lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot <|
    mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 <| Nat.factorial_ne_zero n

Lower bound on root multiplicity via vanishing derivatives in characteristic zero

Informal description

Let $R$ be a commutative ring of characteristic zero, $p \in R[X]$ a nonzero polynomial, $t \in R$, and $n \in \mathbb{N}$. If for all $m \leq n$, the $m$-th derivative of $p$ evaluated at $t$ is zero (i.e., $(\partial^m p)(t) = 0$), then $n$ is strictly less than the root multiplicity of $t$ in $p$ (i.e., $n < \text{rootMultiplicity}(p, t)$).

Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative theorem

 [CharZero R] {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) : n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t

Full source

theorem lt_rootMultiplicity_iff_isRoot_iterate_derivative
    [CharZero R] {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) :
    n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t :=
  ⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| Nat.lt_of_le_of_lt hm hn,
    fun hr ↦ lt_rootMultiplicity_of_isRoot_iterate_derivative h hr⟩

Characterization of root multiplicity via vanishing derivatives in characteristic zero: $n < \text{rootMultiplicity}(p, t) \leftrightarrow (\forall m \leq n, \partial^m p(t) = 0)$

Informal description

Let $R$ be a commutative ring of characteristic zero, $p \in R[X]$ a nonzero polynomial, $t \in R$, and $n \in \mathbb{N}$. Then $n$ is strictly less than the root multiplicity of $t$ in $p$ if and only if for all $m \leq n$, the $m$-th derivative of $p$ evaluated at $t$ is zero, i.e., $(\partial^m p)(t) = 0$.

Polynomial.isRoot_of_isRoot_of_dvd_derivative_mul theorem

[CharZero R] {f g : R[X]} (hf0 : f ≠ 0) (hfd : f ∣ f.derivative * g) {a : R} (haf : f.IsRoot a) : g.IsRoot a

Full source

/-- A sufficient condition for the set of roots of a nonzero polynomial `f` to be a subset of the
set of roots of `g` is that `f` divides `f.derivative * g`. Over an algebraically closed field of
characteristic zero, this is also a necessary condition.
See `isRoot_of_isRoot_iff_dvd_derivative_mul` -/
theorem isRoot_of_isRoot_of_dvd_derivative_mul [CharZero R] {f g : R[X]} (hf0 : f ≠ 0)
    (hfd : f ∣ f.derivative * g) {a : R} (haf : f.IsRoot a) : g.IsRoot a := by
  rcases hfd with ⟨r, hr⟩
  have hdf0 : derivativederivative f ≠ 0 := by
    contrapose! haf
    rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢
    exact not_isRoot_C _ _ <| C_ne_zero.mp hf0
  by_contra hg
  have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)
  have hr' := congr_arg (rootMultiplicity a) hr
  rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf,
    rootMultiplicity_eq_zero hg, add_zero, rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
    Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'
  omega

Root Inclusion via Divisibility of Derivative Product: $f \mid f' \cdot g \Rightarrow \text{roots}(f) \subseteq \text{roots}(g)$

Informal description

Let $R$ be a commutative ring of characteristic zero, and let $f, g \in R[X]$ be polynomials with $f \neq 0$. If $f$ divides $f' \cdot g$ (where $f'$ is the derivative of $f$), then for any root $a \in R$ of $f$, $a$ is also a root of $g$. That is, if $f(a) = 0$, then $g(a) = 0$.

Polynomial.instNormalizationMonoid instance

: NormalizationMonoid R[X]

Full source

instance instNormalizationMonoid : NormalizationMonoid R[X] where
  normUnit p :=
    ⟨C ↑(normUnit p.leadingCoeff), C ↑(normUnit p.leadingCoeff)⁻¹, by
      rw [← RingHom.map_mul, Units.mul_inv, C_1], by rw [← RingHom.map_mul, Units.inv_mul, C_1]⟩
  normUnit_zero := Units.ext (by simp)
  normUnit_mul hp0 hq0 :=
    Units.ext
      (by
        dsimp
        rw [Ne, ← leadingCoeff_eq_zero] at *
        rw [leadingCoeff_mul, normUnit_mul hp0 hq0, Units.val_mul, C_mul])
  normUnit_coe_units u :=
    Units.ext
      (by
        dsimp
        rw [← mul_one u⁻¹, Units.val_mul, Units.eq_inv_mul_iff_mul_eq]
        rcases Polynomial.isUnit_iff.1 ⟨u, rfl⟩ with ⟨_, ⟨w, rfl⟩, h2⟩
        rw [← h2, leadingCoeff_C, normUnit_coe_units, ← C_mul, Units.mul_inv, C_1]
        rfl)

Normalization Monoid Structure on Polynomial Ring $R[X]$

Informal description

The ring of univariate polynomials $R[X]$ over a commutative ring $R$ is a normalization monoid. That is, for any polynomial $p \in R[X]$, there exists a unit $u \in R[X]^\times$ such that $u \cdot p$ is in a normalized form, where the normalization function is an idempotent monoid homomorphism.

Polynomial.coe_normUnit theorem

{p : R[X]} : (normUnit p : R[X]) = C ↑(normUnit p.leadingCoeff)

Full source

@[simp]
theorem coe_normUnit {p : R[X]} : (normUnit p : R[X]) = C ↑(normUnit p.leadingCoeff) := by
  simp [normUnit]

Normalization Unit of Polynomial as Constant Polynomial of Leading Coefficient's Normalization Unit

Informal description

For any polynomial $p \in R[X]$, the normalization unit of $p$ (viewed as an element of $R[X]$) is equal to the constant polynomial obtained by lifting the normalization unit of the leading coefficient of $p$ to $R[X]$. That is, $\text{normUnit}(p) = C(\text{normUnit}(\text{leadingCoeff}(p)))$.

Polynomial.leadingCoeff_normalize theorem

(p : R[X]) : leadingCoeff (normalize p) = normalize (leadingCoeff p)

Full source

@[simp]
theorem leadingCoeff_normalize (p : R[X]) :
    leadingCoeff (normalize p) = normalize (leadingCoeff p) := by simp [normalize_apply]

Leading Coefficient of Normalized Polynomial Equals Normalized Leading Coefficient

Informal description

For any polynomial $p \in R[X]$, the leading coefficient of the normalized polynomial $\text{normalize}(p)$ is equal to the normalization of the leading coefficient of $p$, i.e., \[ \text{leadingCoeff}(\text{normalize}(p)) = \text{normalize}(\text{leadingCoeff}(p)). \]

Polynomial.Monic.normalize_eq_self theorem

{p : R[X]} (hp : p.Monic) : normalize p = p

Full source

theorem Monic.normalize_eq_self {p : R[X]} (hp : p.Monic) : normalize p = p := by
  simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one,
    Units.val_one, Polynomial.C.map_one, mul_one]

Normalization Preserves Monic Polynomials

Informal description

For any monic polynomial $p \in R[X]$, the normalized form of $p$ is equal to $p$ itself, i.e., $\text{normalize}(p) = p$.

Polynomial.roots_normalize theorem

{p : R[X]} : (normalize p).roots = p.roots

Full source

theorem roots_normalize {p : R[X]} : (normalize p).roots = p.roots := by
  rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]

Roots Preservation under Normalization in Polynomial Ring $R[X]$

Informal description

For any polynomial $p \in R[X]$, the multiset of roots of the normalized polynomial $\text{normalize}(p)$ is equal to the multiset of roots of $p$, i.e., \[ \text{roots}(\text{normalize}(p)) = \text{roots}(p). \]

Polynomial.normUnit_X theorem

: normUnit (X : Polynomial R) = 1

Full source

theorem normUnit_X : normUnit (X : Polynomial R) = 1 := by
  have := coe_normUnit (R := R) (p := X)
  rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this

Normalization Unit of $X$ is $1$ in $R[X]$

Informal description

The normalization unit of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to the multiplicative identity $1$.

Polynomial.X_eq_normalize theorem

: (X : Polynomial R) = normalize X

Full source

theorem X_eq_normalize : (X : Polynomial R) = normalize X := by
  simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

Normalization of the Polynomial Variable $X$ in $R[X]$

Informal description

In the polynomial ring $R[X]$, the polynomial variable $X$ is equal to its normalized form, i.e., $X = \text{normalize}(X)$.

Polynomial.degree_pos_of_ne_zero_of_nonunit theorem

(hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 < degree p

Full source

theorem degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 < degree p :=
  lt_of_not_ge fun h => by
    rw [eq_C_of_degree_le_zero h] at hp0 hp
    exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))

Nonzero Non-unit Polynomials Have Positive Degree

Informal description

For any nonzero polynomial $p \in R[X]$ that is not a unit, the degree of $p$ is strictly positive, i.e., $\deg(p) > 0$.

Polynomial.map_eq_zero theorem

[Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0

Full source

@[simp]
protected theorem map_eq_zero [Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0 := by
  simp only [Polynomial.ext_iff]
  congr!
  simp [map_eq_zero, coeff_map, coeff_zero]

Polynomial Map is Zero if and only if Polynomial is Zero

Informal description

Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f: R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$, the image of $p$ under the polynomial map induced by $f$ is zero if and only if $p$ is the zero polynomial. That is, $f_*(p) = 0$ if and only if $p = 0$.

Polynomial.map_ne_zero theorem

[Semiring S] [Nontrivial S] {f : R →+* S} (hp : p ≠ 0) : p.map f ≠ 0

Full source

theorem map_ne_zero [Semiring S] [Nontrivial S] {f : R →+* S} (hp : p ≠ 0) : p.map f ≠ 0 :=
  mt (Polynomial.map_eq_zero f).1 hp

Nonzero Polynomials Remain Nonzero Under Ring Homomorphism

Informal description

Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f: R \to S$ be a ring homomorphism. For any nonzero polynomial $p \in R[X]$, the image of $p$ under the polynomial map induced by $f$ is also nonzero. That is, if $p \neq 0$, then $f_*(p) \neq 0$.

Polynomial.degree_map theorem

[Semiring S] [Nontrivial S] (p : R[X]) (f : R →+* S) : degree (p.map f) = degree p

Full source

@[simp]
theorem degree_map [Semiring S] [Nontrivial S] (p : R[X]) (f : R →+* S) :
    degree (p.map f) = degree p :=
  p.degree_map_eq_of_injective f.injective

Degree Preservation under Ring Homomorphism for Polynomials

Informal description

Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f: R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$, the degree of the polynomial $p$ is preserved under the map $f$, i.e., $\deg(f_*(p)) = \deg(p)$.

Polynomial.natDegree_map theorem

[Semiring S] [Nontrivial S] (f : R →+* S) : natDegree (p.map f) = natDegree p

Full source

@[simp]
theorem natDegree_map [Semiring S] [Nontrivial S] (f : R →+* S) :
    natDegree (p.map f) = natDegree p :=
  natDegree_eq_of_degree_eq (degree_map _ f)

Natural Degree Preservation under Ring Homomorphism for Polynomials

Informal description

Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f: R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$, the natural degree of the polynomial $p$ is preserved under the map $f$, i.e., $\text{natDegree}(f_*(p)) = \text{natDegree}(p)$.

Polynomial.leadingCoeff_map theorem

[Semiring S] [Nontrivial S] (f : R →+* S) : leadingCoeff (p.map f) = f (leadingCoeff p)

Full source

@[simp]
theorem leadingCoeff_map [Semiring S] [Nontrivial S] (f : R →+* S) :
    leadingCoeff (p.map f) = f (leadingCoeff p) := by
  simp only [← coeff_natDegree, coeff_map f, natDegree_map]

Leading Coefficient Preservation under Ring Homomorphism for Polynomials

Informal description

Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f: R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$, the leading coefficient of the polynomial $p$ under the map $f$ is equal to $f$ applied to the leading coefficient of $p$, i.e., $\text{leadingCoeff}(f_*(p)) = f(\text{leadingCoeff}(p))$.

Polynomial.monic_map_iff theorem

[Semiring S] [Nontrivial S] {f : R →+* S} {p : R[X]} : (p.map f).Monic ↔ p.Monic

Full source

theorem monic_map_iff [Semiring S] [Nontrivial S] {f : R →+* S} {p : R[X]} :
    (p.map f).Monic ↔ p.Monic := by
  rw [Monic, leadingCoeff_map, ← f.map_one, Function.Injective.eq_iff f.injective, Monic]

Preservation of Monicity under Ring Homomorphism for Polynomials

Informal description

Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f: R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$, the polynomial $f_*(p) \in S[X]$ is monic if and only if $p$ is monic.

Polynomial.isUnit_iff_degree_eq_zero theorem

: IsUnit p ↔ degree p = 0

Full source

theorem isUnit_iff_degree_eq_zero : IsUnitIsUnit p ↔ degree p = 0 :=
  ⟨degree_eq_zero_of_isUnit, fun h =>
    have : degree p ≤ 0 := by simp [*, le_refl]
    have hc : coeff p 0 ≠ 0 := fun hc => by
      rw [eq_C_of_degree_le_zero this, hc] at h; simp only [map_zero] at h; contradiction
    isUnit_iff_dvd_one.2
      ⟨C (coeff p 0)⁻¹, by
        conv in p => rw [eq_C_of_degree_le_zero this]
        rw [← C_mul, mul_inv_cancel₀ hc, C_1]⟩⟩

Characterization of Units in Polynomial Ring: $\text{IsUnit}(p) \leftrightarrow \deg(p) = 0$

Informal description

A polynomial $p$ over a field $K$ is a unit in the polynomial ring $K[X]$ if and only if its degree is zero, i.e., $p$ is a nonzero constant polynomial.

Polynomial.div definition

(p q : R[X])

Full source

/-- Division of polynomials. See `Polynomial.divByMonic` for more details. -/
def div (p q : R[X]) :=
  C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹))

Polynomial division over a field

Informal description

Given two polynomials $ p $ and $ q $ over a field $ R $, the division $ p / q $ is defined as $ C(\text{leadingCoeff } q)^{-1} \cdot (p \div_{\text{M}} (q \cdot C(\text{leadingCoeff } q)^{-1})) $, where $ \div_{\text{M}} $ denotes division by a monic polynomial (via `divByMonic`), and $ C $ is the constant polynomial embedding.

Polynomial.mod definition

(p q : R[X])

Full source

/-- Remainder of polynomial division. See `Polynomial.modByMonic` for more details. -/
def mod (p q : R[X]) :=
  p %ₘ (q * C (leadingCoeff q)⁻¹)

Polynomial remainder function

Informal description

The function `mod` computes the remainder when a polynomial $ p $ is divided by a polynomial $ q $, where $ q $ is first normalized by multiplying it with the inverse of its leading coefficient. Specifically, $ p \mod q = p \mod_{\text{m}} (q \cdot C(\text{lc}(q)^{-1})) $, where $ \text{lc}(q) $ is the leading coefficient of $ q $ and $ C $ is the constant polynomial embedding. If $ q $ is zero, the result is $ p $.

Polynomial.instDiv instance

: Div R[X]

Full source

instance : Div R[X] :=
  ⟨div⟩

Division Operation on Polynomials over a Field

Informal description

For any field $R$, the ring of univariate polynomials $R[X]$ is equipped with a division operation.

Polynomial.instMod instance

: Mod R[X]

Full source

instance : Mod R[X] :=
  ⟨mod⟩

Modulus Operation on Polynomials over a Field

Informal description

For any field $K$, the ring of univariate polynomials $K[X]$ is equipped with a modulus operation, where for polynomials $p$ and $q$, the remainder $p \mod q$ is computed as $p \mod_{\text{m}} (q \cdot C(\text{lc}(q)^{-1}))$, with $\text{lc}(q)$ being the leading coefficient of $q$ and $C$ the constant polynomial embedding. If $q$ is zero, the result is $p$.

Polynomial.div_def theorem

: p / q = C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹))

Full source

theorem div_def : p / q = C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹)) :=
  rfl

Definition of Polynomial Division over a Field

Informal description

For any field $K$ and polynomials $p, q \in K[X]$, the division $p / q$ is defined as $C(\text{lc}(q)^{-1}) \cdot (p \div_{\text{m}} (q \cdot C(\text{lc}(q)^{-1})))$, where $\text{lc}(q)$ is the leading coefficient of $q$, $C$ is the constant polynomial embedding, and $\div_{\text{m}}$ denotes division by a monic polynomial.

Polynomial.mod_def theorem

: p % q = p %ₘ (q * C (leadingCoeff q)⁻¹)

Full source

theorem mod_def : p % q = p %ₘ (q * C (leadingCoeff q)⁻¹) := rfl

Definition of Polynomial Modulus via Monic Scaling

Informal description

For any field $K$ and polynomials $p, q \in K[X]$, the modulus operation $p \% q$ is defined as the remainder of $p$ divided by the monic polynomial obtained by scaling $q$ with the inverse of its leading coefficient, i.e., $p \% q = p \%_{\text{m}} (q \cdot C(\text{lc}(q)^{-1}))$, where $\text{lc}(q)$ is the leading coefficient of $q$ and $C$ is the constant polynomial embedding.

Polynomial.modByMonic_eq_mod theorem

(p : R[X]) (hq : Monic q) : p %ₘ q = p % q

Full source

theorem modByMonic_eq_mod (p : R[X]) (hq : Monic q) : p %ₘ q = p % q :=
  show p %ₘ q = p %ₘ (q * C (leadingCoeff q)⁻¹) by
    simp only [Monic.def.1 hq, inv_one, mul_one, C_1]

Equality of Remainders: Monic vs Standard Division ($p \%_{\text{m}} q = p \% q$)

Informal description

For any polynomial $p$ over a ring $R$ and any monic polynomial $q$, the remainder of $p$ divided by $q$ using monic division equals the remainder of $p$ divided by $q$ using standard polynomial division, i.e., $p \%_{\text{m}} q = p \% q$.

Polynomial.divByMonic_eq_div theorem

(p : R[X]) (hq : Monic q) : p /ₘ q = p / q

Full source

theorem divByMonic_eq_div (p : R[X]) (hq : Monic q) : p /ₘ q = p / q :=
  show p /ₘ q = C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹)) by
    simp only [Monic.def.1 hq, inv_one, C_1, one_mul, mul_one]

Equality of Monic Division and Polynomial Division for Monic Polynomials

Informal description

For any polynomial $p$ over a ring $R$ and a monic polynomial $q$, the division of $p$ by $q$ using the monic division algorithm (`divByMonic`) equals the division of $p$ by $q$ in the polynomial ring $R[X]$.

Polynomial.mod_X_sub_C_eq_C_eval theorem

(p : R[X]) (a : R) : p % (X - C a) = C (p.eval a)

Full source

theorem mod_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p % (X - C a) = C (p.eval a) :=
  modByMonic_eq_mod p (monic_X_sub_C a) ▸ modByMonic_X_sub_C_eq_C_eval _ _

Remainder Theorem: $p \mod (X - a) = p(a)$

Informal description

For any polynomial $p$ over a ring $R$ and any element $a \in R$, the remainder when $p$ is divided by the polynomial $X - a$ is equal to the constant polynomial $C(p(a))$, where $p(a)$ denotes the evaluation of $p$ at $a$.

Polynomial.mul_div_eq_iff_isRoot theorem

: (X - C a) * (p / (X - C a)) = p ↔ IsRoot p a

Full source

theorem mul_div_eq_iff_isRoot : (X - C a) * (p / (X - C a)) = p ↔ IsRoot p a :=
  divByMonic_eq_div p (monic_X_sub_C a) ▸ mul_divByMonic_eq_iff_isRoot

Factorization Identity: $(X - a) \cdot (p/(X - a)) = p \iff p(a) = 0$

Informal description

For any polynomial $p$ over a field $R$ and any element $a \in R$, the product of the linear polynomial $(X - a)$ and the quotient $p / (X - a)$ equals $p$ if and only if $a$ is a root of $p$ (i.e., $p(a) = 0$). In other words: $$(X - a) \cdot \left(\frac{p}{X - a}\right) = p \iff p(a) = 0.$$

Polynomial.instEuclideanDomain instance

: EuclideanDomain R[X]

Full source

instance instEuclideanDomain : EuclideanDomain R[X] :=
  { Polynomial.commRing,
    Polynomial.nontrivial with
    quotient := (· / ·)
    quotient_zero := by simp [div_def]
    remainder := (· % ·)
    r := _
    r_wellFounded := degree_lt_wf
    quotient_mul_add_remainder_eq := quotient_mul_add_remainder_eq_aux
    remainder_lt := fun _ _ hq => remainder_lt_aux _ hq
    mul_left_not_lt := fun _ _ hq => not_lt_of_ge (degree_le_mul_left _ hq) }

Polynomial Rings over Fields are Euclidean Domains

Informal description

For any field $R$, the ring of univariate polynomials $R[X]$ is a Euclidean domain.

Polynomial.mod_eq_self_iff theorem

(hq0 : q ≠ 0) : p % q = p ↔ degree p < degree q

Full source

theorem mod_eq_self_iff (hq0 : q ≠ 0) : p % q = p ↔ degree p < degree q :=
  ⟨fun h => h ▸ EuclideanDomain.mod_lt _ hq0, fun h => by
    classical
    have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]⟩

Remainder Equals Dividend if and only if Degree Condition Holds

Informal description

For any nonzero polynomial $q$ in $R[X]$, the remainder of $p$ divided by $q$ equals $p$ if and only if the degree of $p$ is strictly less than the degree of $q$, i.e., $p \% q = p \leftrightarrow \deg p < \deg q$.

Polynomial.div_eq_zero_iff theorem

(hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q

Full source

theorem div_eq_zero_iff (hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q :=
  ⟨fun h => by
    have := EuclideanDomain.div_add_mod p q
    rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this,
  fun h => by
    have hlt : degree p < degree (q * C (leadingCoeff q)⁻¹) := by
      rwa [degree_mul_leadingCoeff_inv q hq0]
    have hm : Monic (q * C (leadingCoeff q)⁻¹) := monic_mul_leadingCoeff_inv hq0
    rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, mul_zero]⟩

Quotient Zero Condition in Polynomial Division: $\deg p < \deg q \leftrightarrow p/q = 0$

Informal description

For any nonzero polynomial $q$ in $R[X]$, the quotient $p / q$ is zero if and only if the degree of $p$ is strictly less than the degree of $q$, i.e., $p / q = 0 \leftrightarrow \deg p < \deg q$.

Polynomial.degree_add_div theorem

(hq0 : q ≠ 0) (hpq : degree q ≤ degree p) : degree q + degree (p / q) = degree p

Full source

theorem degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) :
    degree q + degree (p / q) = degree p := by
  have : degree (p % q) < degree (q * (p / q)) :=
    calc
      degree (p % q) < degree q := EuclideanDomain.mod_lt _ hq0
      _ ≤ _ := degree_le_mul_left _ (mt (div_eq_zero_iff hq0).1 (not_lt_of_ge hpq))

  conv_rhs =>
    rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]

Degree Addition Formula for Polynomial Division: $\deg q + \deg(p/q) = \deg p$

Informal description

For any nonzero polynomial $q$ in $R[X]$ and any polynomial $p$ with $\deg q \leq \deg p$, the sum of the degrees of $q$ and the quotient $p/q$ equals the degree of $p$, i.e., \[ \deg q + \deg(p/q) = \deg p. \]

Polynomial.degree_div_le theorem

(p q : R[X]) : degree (p / q) ≤ degree p

Full source

theorem degree_div_le (p q : R[X]) : degree (p / q) ≤ degree p := by
  by_cases hq : q = 0
  · simp [hq]
  · rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]; exact degree_divByMonic_le _ _

Degree Bound for Polynomial Division: $\deg(p/q) \leq \deg p$

Informal description

For any polynomials $p$ and $q$ over a field $R$, the degree of the quotient $p/q$ is less than or equal to the degree of $p$, i.e., \[ \deg(p/q) \leq \deg p. \]

Polynomial.degree_div_lt theorem

(hp : p ≠ 0) (hq : 0 < degree q) : degree (p / q) < degree p

Full source

theorem degree_div_lt (hp : p ≠ 0) (hq : 0 < degree q) : degree (p / q) < degree p := by
  have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
  rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]
  exact degree_divByMonic_lt _ (monic_mul_leadingCoeff_inv hq0) hp
    (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)

Degree Strict Inequality for Polynomial Division: $\deg(p / q) < \deg p$

Informal description

For any polynomials $p$ and $q$ over a field $R$, if $p$ is nonzero and $q$ has positive degree, then the degree of the quotient $p / q$ is strictly less than the degree of $p$, i.e., \[ \deg(p / q) < \deg p. \]

Polynomial.isUnit_map theorem

[Field k] (f : R →+* k) : IsUnit (p.map f) ↔ IsUnit p

Full source

theorem isUnit_map [Field k] (f : R →+* k) : IsUnitIsUnit (p.map f) ↔ IsUnit p := by
  simp_rw [isUnit_iff_degree_eq_zero, degree_map]

Unit Preservation under Field Homomorphism for Polynomials

Informal description

Let $R$ and $k$ be fields, and let $f: R \to k$ be a ring homomorphism. For any polynomial $p \in R[X]$, the polynomial $p$ is a unit in $R[X]$ if and only if its image under the map $f$ is a unit in $k[X]$. In other words, $p$ is invertible in $R[X]$ precisely when $f_*(p)$ is invertible in $k[X]$.

Polynomial.map_div theorem

[Field k] (f : R →+* k) : (p / q).map f = p.map f / q.map f

Full source

theorem map_div [Field k] (f : R →+* k) : (p / q).map f = p.map f / q.map f := by
  if hq0 : q = 0 then simp [hq0]
  else
    rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
      Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]

Ring Homomorphism Commutes with Polynomial Division: $f(p/q) = f(p)/f(q)$

Informal description

Let $R$ and $k$ be fields, and let $f \colon R \to k$ be a ring homomorphism. For any polynomials $p, q \in R[X]$, the image of the quotient $p/q$ under $f$ equals the quotient of the images, i.e., \[ f_*(p/q) = f_*(p)/f_*(q). \]

Polynomial.map_mod theorem

[Field k] (f : R →+* k) : (p % q).map f = p.map f % q.map f

Full source

theorem map_mod [Field k] (f : R →+* k) : (p % q).map f = p.map f % q.map f := by
  by_cases hq0 : q = 0
  · simp [hq0]
  · rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]

Ring Homomorphism Commutes with Polynomial Remainder Operation

Informal description

Let $R$ and $k$ be fields, and let $f \colon R \to k$ be a ring homomorphism. For any polynomials $p, q \in R[X]$, the image under $f$ of the remainder $p \mod q$ equals the remainder of the images, i.e., \[ f(p \mod q) = f(p) \mod f(q). \]

Polynomial.natDegree_mod_lt theorem

[Field k] (p : k[X]) {q : k[X]} (hq : q.natDegree ≠ 0) : (p % q).natDegree < q.natDegree

Full source

lemma natDegree_mod_lt [Field k] (p : k[X]) {q : k[X]} (hq : q.natDegree ≠ 0) :
    (p % q).natDegree < q.natDegree := by
  have hq' : q.leadingCoeff ≠ 0 := by
    rw [leadingCoeff_ne_zero]
    contrapose! hq
    simp [hq]
  rw [mod_def]
  refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_
  · refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    rw [mul_inv_eq_one₀ hq']
  · contrapose! hq
    rw [← natDegree_mul_C_eq_of_mul_eq_one ((inv_mul_eq_one₀ hq').mpr rfl)]
    simp [hq]
  · exact natDegree_mul_C_le q q.leadingCoeff⁻¹

Degree Bound for Polynomial Remainder: $\deg(p \mod q) < \deg q$ for $\deg q \neq 0$

Informal description

Let $k$ be a field and $p, q \in k[X]$ be polynomials such that $q$ has nonzero degree. Then the degree of the remainder $p \mod q$ is strictly less than the degree of $q$, i.e., $\deg(p \mod q) < \deg q$.

Polynomial.gcd_map theorem

[Field k] [DecidableEq R] [DecidableEq k] (f : R →+* k) : gcd (p.map f) (q.map f) = (gcd p q).map f

Full source

theorem gcd_map [Field k] [DecidableEq R] [DecidableEq k] (f : R →+* k) :
    gcd (p.map f) (q.map f) = (gcd p q).map f :=
  GCD.induction p q (fun x => by simp_rw [Polynomial.map_zero, EuclideanDomain.gcd_zero_left])
    fun x y _ ih => by rw [gcd_val, ← map_mod, ih, ← gcd_val]

GCD Preservation under Ring Homomorphism: $\gcd(f(p), f(q)) = f(\gcd(p, q))$

Informal description

Let $R$ and $k$ be fields with decidable equality, and let $f \colon R \to k$ be a ring homomorphism. For any polynomials $p, q \in R[X]$, the greatest common divisor of the images $f(p)$ and $f(q)$ equals the image of the greatest common divisor of $p$ and $q$ under $f$, i.e., \[ \gcd(f(p), f(q)) = f(\gcd(p, q)). \]

Polynomial.eval₂_gcd_eq_zero theorem

 [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k} (hf : f.eval₂ ϕ α = 0) (hg : g.eval₂ ϕ α = 0) :
  (EuclideanDomain.gcd f g).eval₂ ϕ α = 0

Full source

theorem eval₂_gcd_eq_zero [CommSemiring k] [DecidableEq R]
    {ϕ : R →+* k} {f g : R[X]} {α : k} (hf : f.eval₂ ϕ α = 0)
    (hg : g.eval₂ ϕ α = 0) : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0 := by
  rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]

Evaluation of GCD at Common Zero Point

Informal description

Let $R$ and $k$ be commutative semirings with decidable equality, and let $\phi : R \to k$ be a ring homomorphism. For any univariate polynomials $f, g \in R[X]$ and any element $\alpha \in k$, if both $f$ and $g$ evaluate to zero at $\alpha$ under $\phi$ (i.e., $\text{eval}_\phi(f, \alpha) = 0$ and $\text{eval}_\phi(g, \alpha) = 0$), then the greatest common divisor $\gcd(f, g)$ also evaluates to zero at $\alpha$ under $\phi$ (i.e., $\text{eval}_\phi(\gcd(f, g), \alpha) = 0$).

Polynomial.eval_gcd_eq_zero theorem

[DecidableEq R] {f g : R[X]} {α : R} (hf : f.eval α = 0) (hg : g.eval α = 0) : (EuclideanDomain.gcd f g).eval α = 0

Full source

theorem eval_gcd_eq_zero [DecidableEq R] {f g : R[X]} {α : R}
    (hf : f.eval α = 0) (hg : g.eval α = 0) : (EuclideanDomain.gcd f g).eval α = 0 :=
  eval₂_gcd_eq_zero hf hg

Evaluation of GCD at Common Root: $\gcd(f, g)(\alpha) = 0$ when $f(\alpha) = g(\alpha) = 0$

Informal description

Let $R$ be a commutative semiring with decidable equality, and let $f, g \in R[X]$ be univariate polynomials. For any element $\alpha \in R$, if both $f$ and $g$ evaluate to zero at $\alpha$ (i.e., $f(\alpha) = 0$ and $g(\alpha) = 0$), then the greatest common divisor $\gcd(f, g)$ also evaluates to zero at $\alpha$ (i.e., $\gcd(f, g)(\alpha) = 0$).

Polynomial.root_left_of_root_gcd theorem

 [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k} (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) :
  f.eval₂ ϕ α = 0

Full source

theorem root_left_of_root_gcd [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k}
    (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : f.eval₂ ϕ α = 0 := by
  obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_left f g
  rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

Root of GCD Implies Root of First Polynomial: $(\gcd(f, g))(\alpha) = 0 \Rightarrow f(\alpha) = 0$

Informal description

Let $R$ be a commutative semiring, $k$ a commutative semiring with decidable equality, and $\phi : R \to k$ a ring homomorphism. For any polynomials $f, g \in R[X]$ and any element $\alpha \in k$, if the greatest common divisor $\gcd(f, g)$ satisfies $(\gcd(f, g)).\text{eval}_\phi \alpha = 0$, then $f.\text{eval}_\phi \alpha = 0$.

Polynomial.root_right_of_root_gcd theorem

 [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k} (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) :
  g.eval₂ ϕ α = 0

Full source

theorem root_right_of_root_gcd [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k}
    (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : g.eval₂ ϕ α = 0 := by
  obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_right f g
  rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

Right Root Implication from GCD Root in Polynomial Evaluation

Informal description

Let $R$ and $k$ be commutative semirings with decidable equality, and let $\phi : R \to k$ be a ring homomorphism. For any polynomials $f, g \in R[X]$ and any element $\alpha \in k$, if the evaluation of $\gcd(f, g)$ at $\alpha$ via $\phi$ is zero, then the evaluation of $g$ at $\alpha$ via $\phi$ is also zero. In other words, if $\phi(\gcd(f, g))(\alpha) = 0$, then $\phi(g)(\alpha) = 0$.

Polynomial.root_gcd_iff_root_left_right theorem

 [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k} :
  (EuclideanDomain.gcd f g).eval₂ ϕ α = 0 ↔ f.eval₂ ϕ α = 0 ∧ g.eval₂ ϕ α = 0

Full source

theorem root_gcd_iff_root_left_right [CommSemiring k] [DecidableEq R]
    {ϕ : R →+* k} {f g : R[X]} {α : k} :
    (EuclideanDomain.gcd f g).eval₂ ϕ α = 0 ↔ f.eval₂ ϕ α = 0 ∧ g.eval₂ ϕ α = 0 :=
  ⟨fun h => ⟨root_left_of_root_gcd h, root_right_of_root_gcd h⟩, fun h => eval₂_gcd_eq_zero h.1 h.2⟩

GCD Root Equivalence: $\gcd(f, g)(\alpha) = 0 \Leftrightarrow f(\alpha) = 0 \land g(\alpha) = 0$

Informal description

Let $R$ and $k$ be commutative semirings with decidable equality, and let $\phi : R \to k$ be a ring homomorphism. For any polynomials $f, g \in R[X]$ and any element $\alpha \in k$, the evaluation of $\gcd(f, g)$ at $\alpha$ via $\phi$ is zero if and only if both $f$ and $g$ evaluate to zero at $\alpha$ via $\phi$. In other words: $$ \phi(\gcd(f, g))(\alpha) = 0 \Leftrightarrow \phi(f)(\alpha) = 0 \text{ and } \phi(g)(\alpha) = 0. $$

Polynomial.isRoot_gcd_iff_isRoot_left_right theorem

[DecidableEq R] {f g : R[X]} {α : R} : (EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α

Full source

theorem isRoot_gcd_iff_isRoot_left_right [DecidableEq R] {f g : R[X]} {α : R} :
    (EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α :=
  root_gcd_iff_root_left_right

GCD Root Equivalence: $\gcd(f, g)(\alpha) = 0 \leftrightarrow f(\alpha) = g(\alpha) = 0$

Informal description

For any polynomials $f, g \in R[X]$ over a ring $R$ with decidable equality, and any element $\alpha \in R$, the greatest common divisor $\gcd(f, g)$ has $\alpha$ as a root if and only if both $f$ and $g$ have $\alpha$ as a root. In other words: $$\gcd(f, g)(\alpha) = 0 \leftrightarrow f(\alpha) = 0 \text{ and } g(\alpha) = 0.$$

Polynomial.isCoprime_map theorem

[Field k] (f : R →+* k) : IsCoprime (p.map f) (q.map f) ↔ IsCoprime p q

Full source

theorem isCoprime_map [Field k] (f : R →+* k) : IsCoprimeIsCoprime (p.map f) (q.map f) ↔ IsCoprime p q := by
  classical
  rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]

Coprimality Preservation under Field Homomorphism for Polynomials

Informal description

Let $R$ and $k$ be fields, and let $f \colon R \to k$ be a ring homomorphism. For any polynomials $p, q \in R[X]$, the images $f(p)$ and $f(q)$ are coprime in $k[X]$ if and only if $p$ and $q$ are coprime in $R[X]$.

Polynomial.mem_roots_map theorem

[CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) : x ∈ (p.map f).roots ↔ p.eval₂ f x = 0

Full source

theorem mem_roots_map [CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) :
    x ∈ (p.map f).rootsx ∈ (p.map f).roots ↔ p.eval₂ f x = 0 := by
  rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]

Characterization of Roots Under Polynomial Map: $x \in (p.map(f)).roots \leftrightarrow p.eval₂(f, x) = 0$

Informal description

Let $R$ and $k$ be commutative rings with $k$ being a domain, and let $f: R \to k$ be a ring homomorphism. For any nonzero polynomial $p \in R[X]$ and any element $x \in k$, $x$ is a root of the polynomial $p.map(f)$ (i.e., $x \in (p.map(f)).roots$) if and only if the evaluation of $p$ at $x$ via $f$ is zero (i.e., $p.eval₂(f, x) = 0$).

Polynomial.rootSet_monomial theorem

 [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) : (monomial n a).rootSet S = {0}

Full source

theorem rootSet_monomial [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R}
    (ha : a ≠ 0) : (monomial n a).rootSet S = {0} := by
  classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

Root Set of Monomial is $\{0\}$ in Domain Algebra

Informal description

Let $R$ and $S$ be commutative rings with $S$ being a domain, and let $S$ be an $R$-algebra. For any nonzero natural number $n$ and any nonzero element $a \in R$, the root set of the monomial $aX^n$ in $S$ is $\{0\}$. That is, the only root of $aX^n$ in $S$ is $0$.

Polynomial.rootSet_C_mul_X_pow theorem

[CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) : rootSet (C a * X ^ n) S = {0}

Full source

theorem rootSet_C_mul_X_pow [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R}
    (ha : a ≠ 0) : rootSet (C a * X ^ n) S = {0} := by
  rw [C_mul_X_pow_eq_monomial, rootSet_monomial hn ha]

Root Set of Monomial $aX^n$ is $\{0\}$ in Domain Algebra

Informal description

Let $R$ and $S$ be commutative rings with $S$ being a domain, and let $S$ be an $R$-algebra. For any nonzero natural number $n$ and any nonzero element $a \in R$, the root set of the polynomial $aX^n$ in $S$ is $\{0\}$. That is, the only root of $aX^n$ in $S$ is $0$.

Polynomial.rootSet_X_pow theorem

[CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) : (X ^ n : R[X]).rootSet S = {0}

Full source

theorem rootSet_X_pow [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) :
    (X ^ n : R[X]).rootSet S = {0} := by
  rw [← one_mul (X ^ n : R[X]), ← C_1, rootSet_C_mul_X_pow hn]
  exact one_ne_zero

Root Set of $X^n$ is $\{0\}$ in Domain Algebra

Informal description

Let $R$ and $S$ be commutative rings with $S$ being a domain, and let $S$ be an $R$-algebra. For any nonzero natural number $n$, the root set of the polynomial $X^n$ in $S$ is $\{0\}$. That is, the only root of $X^n$ in $S$ is $0$.

Polynomial.rootSet_prod theorem

 [CommRing S] [IsDomain S] [Algebra R S] {ι : Type*} (f : ι → R[X]) (s : Finset ι) (h : s.prod f ≠ 0) :
  (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S

Full source

theorem rootSet_prod [CommRing S] [IsDomain S] [Algebra R S] {ι : Type*} (f : ι → R[X])
    (s : Finset ι) (h : s.prod f ≠ 0) : (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S := by
  classical
  simp only [rootSet, aroots, ← Finset.mem_coe]
  rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
  rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]

Root Set of Product of Polynomials Equals Union of Root Sets

Informal description

Let $R$ and $S$ be commutative rings with $S$ being a domain, and let $f : R \to S$ be an algebra homomorphism. For any finite set $\{f_i\}_{i \in \iota}$ of nonzero polynomials in $R[X]$, the root set of their product $\prod_{i \in \iota} f_i$ in $S$ is equal to the union of the root sets of each $f_i$ in $S$. That is, $$\left(\prod_{i \in \iota} f_i\right).\text{rootSet}(S) = \bigcup_{i \in \iota} (f_i.\text{rootSet}(S)).$$

Polynomial.roots_C_mul_X_sub_C theorem

(b : R) (ha : a ≠ 0) : (C a * X - C b).roots = {a⁻¹ * b}

Full source

theorem roots_C_mul_X_sub_C (b : R) (ha : a ≠ 0) : (C a * X - C b).roots = {a⁻¹ * b} := by
  simp [roots_C_mul_X_sub_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

Roots of the linear polynomial $aX - b$ are $\{a^{-1}b\}$

Informal description

Let $R$ be a field, and let $a, b \in R$ with $a \neq 0$. The roots of the linear polynomial $aX - b$ (where $X$ is the polynomial variable) are precisely $\{a^{-1}b\}$.

Polynomial.roots_C_mul_X_add_C theorem

(b : R) (ha : a ≠ 0) : (C a * X + C b).roots = {-(a⁻¹ * b)}

Full source

theorem roots_C_mul_X_add_C (b : R) (ha : a ≠ 0) : (C a * X + C b).roots = {-(a⁻¹ * b)} := by
  simp [roots_C_mul_X_add_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

Roots of the linear polynomial $aX + b$ are $\{-a^{-1}b\}$

Informal description

Let $R$ be a field and $a, b \in R$ with $a \neq 0$. The roots of the linear polynomial $aX + b$ (where $X$ is the polynomial variable) are precisely $\{-a^{-1}b\}$.

Polynomial.roots_degree_eq_one theorem

(h : degree p = 1) : p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}

Full source

theorem roots_degree_eq_one (h : degree p = 1) : p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)} := by
  rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [h])]
  have : p.coeff 1 ≠ 0 := coeff_ne_zero_of_eq_degree h
  simp [roots_C_mul_X_add_C _ this]

Roots of degree one polynomial: $\text{roots}(p) = \{ -p_1^{-1}p_0 \}$ when $\deg p = 1$

Informal description

Let $R$ be a field and $p \in R[X]$ be a polynomial of degree 1. Then the roots of $p$ form the singleton set $\{ - (p_1)^{-1} p_0 \}$, where $p_1$ and $p_0$ are the coefficients of $X^1$ and $X^0$ in $p$ respectively.

Polynomial.exists_root_of_degree_eq_one theorem

(h : degree p = 1) : ∃ x, IsRoot p x

Full source

theorem exists_root_of_degree_eq_one (h : degree p = 1) : ∃ x, IsRoot p x :=
  ⟨-((p.coeff 1)⁻¹ * p.coeff 0), by
    rw [← mem_roots (by simp [← zero_le_degree_iff, h])]
    simp [roots_degree_eq_one h]⟩

Existence of Root for Degree One Polynomials

Informal description

For any polynomial $p$ over a field $R$ with $\deg(p) = 1$, there exists an element $x \in R$ such that $p(x) = 0$.

Polynomial.coeff_inv_units theorem

(u : R[X]ˣ) (n : ℕ) : ((↑u : R[X]).coeff n)⁻¹ = (↑u⁻¹ : R[X]).coeff n

Full source

theorem coeff_inv_units (u : R[X]R[X]ˣ) (n : ℕ) : ((↑u : R[X]).coeff n)⁻¹ = (↑u⁻¹ : R[X]).coeff n := by
  rw [eq_C_of_degree_eq_zero (degree_coe_units u), eq_C_of_degree_eq_zero (degree_coe_units u⁻¹),
    coeff_C, coeff_C, inv_eq_one_div]
  split_ifs
  · rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero,
        coeff_zero_eq_eval_zero, ← eval_mul, ← Units.val_mul, inv_mul_cancel]
    simp
  · simp

Inverse of Polynomial Unit Coefficients: $(\text{coeff}(u, n))^{-1} = \text{coeff}(u^{-1}, n)$

Informal description

For any unit $u$ in the polynomial ring $R[X]$ and any natural number $n$, the coefficient of $X^n$ in the inverse of $u$ is equal to the inverse of the coefficient of $X^n$ in $u$. In mathematical notation: $$(\text{coeff}(u, n))^{-1} = \text{coeff}(u^{-1}, n)$$

Polynomial.monic_normalize theorem

[DecidableEq R] (hp0 : p ≠ 0) : Monic (normalize p)

Full source

theorem monic_normalize [DecidableEq R] (hp0 : p ≠ 0) : Monic (normalize p) := by
  rw [Ne, ← leadingCoeff_eq_zero, ← Ne, ← isUnit_iff_ne_zero] at hp0
  rw [Monic, leadingCoeff_normalize, normalize_eq_one]
  apply hp0

Normalized Polynomial is Monic for Nonzero Polynomials

Informal description

For any nonzero polynomial $p \in R[X]$, the normalized form of $p$ is monic, i.e., the leading coefficient of $\text{normalize}(p)$ is equal to $1$.

Polynomial.leadingCoeff_div theorem

(hpq : q.degree ≤ p.degree) : (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Full source

theorem leadingCoeff_div (hpq : q.degree ≤ p.degree) :
    (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff := by
  by_cases hq : q = 0
  · simp [hq]
  rw [div_def, leadingCoeff_mul, leadingCoeff_C,
    leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _, mul_comm,
    div_eq_mul_inv]
  rwa [degree_mul_leadingCoeff_inv q hq]

Leading Coefficient of Polynomial Quotient: $\text{lc}(p / q) = \text{lc}(p) / \text{lc}(q)$

Informal description

For any polynomials $p$ and $q$ over a field $K$ such that $\deg(q) \leq \deg(p)$, the leading coefficient of the quotient $p / q$ is equal to the quotient of the leading coefficients of $p$ and $q$, i.e., \[ \text{lc}(p / q) = \text{lc}(p) / \text{lc}(q). \]

Polynomial.div_C_mul theorem

: p / (C a * q) = C a⁻¹ * (p / q)

Full source

theorem div_C_mul : p / (C a * q) = C a⁻¹ * (p / q) := by
  by_cases ha : a = 0
  · simp [ha]
  simp only [div_def, leadingCoeff_mul, mul_inv, leadingCoeff_C, C.map_mul, mul_assoc]
  congr 3
  rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]

Division by Constant Multiple in Polynomial Ring: $p / (a \cdot q) = a^{-1} \cdot (p / q)$

Informal description

For any polynomial $p$ and nonzero constant $a$ in a field $R$, and any polynomial $q$ in $R[X]$, the division of $p$ by the product of the constant polynomial $C(a)$ and $q$ equals the product of the constant polynomial $C(a^{-1})$ and the division of $p$ by $q$, i.e., \[ p / (C(a) \cdot q) = C(a^{-1}) \cdot (p / q). \]

Polynomial.C_mul_dvd theorem

(ha : a ≠ 0) : C a * p ∣ q ↔ p ∣ q

Full source

theorem C_mul_dvd (ha : a ≠ 0) : CC a * p ∣ qC a * p ∣ q ↔ p ∣ q :=
  ⟨fun h => dvd_trans (dvd_mul_left _ _) h, fun ⟨r, hr⟩ =>
    ⟨C a⁻¹ * r, by
      rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]⟩⟩

Divisibility by Constant Multiple: $C(a) \cdot p \mid q \leftrightarrow p \mid q$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a commutative ring $R$ and any polynomials $p, q \in R[X]$, the constant polynomial $C(a)$ multiplied by $p$ divides $q$ if and only if $p$ divides $q$.

Polynomial.dvd_C_mul theorem

(ha : a ≠ 0) : p ∣ Polynomial.C a * q ↔ p ∣ q

Full source

theorem dvd_C_mul (ha : a ≠ 0) : p ∣ Polynomial.C a * qp ∣ Polynomial.C a * q ↔ p ∣ q :=
  ⟨fun ⟨r, hr⟩ =>
    ⟨C a⁻¹ * r, by
      rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_cancel₀ ha, C.map_one,
        one_mul]⟩,
    fun h => dvd_trans h (dvd_mul_left _ _)⟩

Divisibility by Constant Multiple in Polynomial Rings: $p \mid a \cdot q \leftrightarrow p \mid q$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a field $R$ and any polynomials $p, q \in R[X]$, the polynomial $p$ divides the product of the constant polynomial $C(a)$ and $q$ if and only if $p$ divides $q$.

Polynomial.coe_normUnit_of_ne_zero theorem

[DecidableEq R] (hp : p ≠ 0) : (normUnit p : R[X]) = C p.leadingCoeff⁻¹

Full source

theorem coe_normUnit_of_ne_zero [DecidableEq R] (hp : p ≠ 0) :
    (normUnit p : R[X]) = C p.leadingCoeff⁻¹ := by
  have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp
  simp [CommGroupWithZero.coe_normUnit _ this]

Normalization Unit of Nonzero Polynomial as Inverse Leading Coefficient

Informal description

For any nonzero polynomial $p \in R[X]$ over a field $R$, the normalization unit of $p$ (viewed as an element of $R[X]$) is equal to the constant polynomial formed by the multiplicative inverse of the leading coefficient of $p$, i.e., $\text{normUnit}(p) = C(\text{leadingCoeff}(p)^{-1})$.

Polynomial.map_dvd_map' theorem

[Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map f ↔ x ∣ y

Full source

theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map fx.map f ∣ y.map f ↔ x ∣ y := by
  by_cases H : x = 0
  · rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
  · classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

Divisibility Preservation under Polynomial Ring Homomorphisms: $f(x) \mid f(y) \leftrightarrow x \mid y$

Informal description

Let $R$ be a commutative ring and $k$ be a field. For any ring homomorphism $f \colon R \to k$ and any polynomials $x, y \in R[X]$, the image polynomial $f(x)$ divides $f(y)$ in $k[X]$ if and only if $x$ divides $y$ in $R[X]$.

Polynomial.degree_normalize theorem

[DecidableEq R] : degree (normalize p) = degree p

Full source

@[simp]
theorem degree_normalize [DecidableEq R] : degree (normalize p) = degree p := by
  simp [normalize_apply]

Degree Preservation under Normalization of Polynomials

Informal description

For any polynomial $p$ over a commutative ring $R$ with decidable equality, the degree of the normalized polynomial $\text{normalize}(p)$ is equal to the degree of $p$, i.e., $\deg(\text{normalize}(p)) = \deg(p)$.

Polynomial.prime_of_degree_eq_one theorem

(hp1 : degree p = 1) : Prime p

Full source

theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p := by
  classical
  have : Prime (normalize p) :=
    Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
      (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp [degree_zero]))
  exact (normalize_associated _).prime this

Linear Polynomials are Prime in $R[X]$

Informal description

Let $p$ be a polynomial over a commutative ring $R$ such that $\deg(p) = 1$. Then $p$ is a prime element in the polynomial ring $R[X]$.

Polynomial.irreducible_of_degree_eq_one theorem

(hp1 : degree p = 1) : Irreducible p

Full source

theorem irreducible_of_degree_eq_one (hp1 : degree p = 1) : Irreducible p :=
  (prime_of_degree_eq_one hp1).irreducible

Linear Polynomials are Irreducible in $K[X]$

Informal description

Let $p$ be a polynomial over a field $K$ such that $\deg(p) = 1$. Then $p$ is irreducible in the polynomial ring $K[X]$.

Polynomial.not_irreducible_C theorem

(x : R) : ¬Irreducible (C x)

Full source

theorem not_irreducible_C (x : R) : ¬Irreducible (C x) := by
  by_cases H : x = 0
  · rw [H, C_0]
    exact not_irreducible_zero
  · exact fun hx => hx.not_isUnit <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H

Constant Polynomials Are Not Irreducible

Informal description

For any element $x$ in a semiring $R$, the constant polynomial $C(x) \in R[X]$ is not irreducible.

Polynomial.degree_pos_of_irreducible theorem

(hp : Irreducible p) : 0 < p.degree

Full source

theorem degree_pos_of_irreducible (hp : Irreducible p) : 0 < p.degree :=
  lt_of_not_ge fun hp0 =>
    have := eq_C_of_degree_le_zero hp0
    not_irreducible_C (p.coeff 0) <| this ▸ hp

Irreducible Polynomials Have Positive Degree

Informal description

If a polynomial $p \in R[X]$ is irreducible, then its degree is positive, i.e., $\deg(p) > 0$.

Polynomial.X_sub_C_mul_divByMonic_eq_sub_modByMonic theorem

{K : Type*} [Ring K] (f : K[X]) (a : K) : (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a)

Full source

theorem X_sub_C_mul_divByMonic_eq_sub_modByMonic {K : Type*} [Ring K] (f : K[X]) (a : K) :
    (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a) := by
  rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]
  exact monic_X_sub_C a

Polynomial Division Identity: $(X - a) \cdot (f / (X - a)) = f - (f \mod (X - a))$

Informal description

Let $K$ be a ring and $f \in K[X]$ be a polynomial. For any $a \in K$, the following equality holds: $$(X - a) \cdot (f / (X - a)) = f - (f \mod (X - a))$$ where $f / (X - a)$ denotes the quotient when $f$ is divided by the monic polynomial $X - a$, and $f \mod (X - a)$ denotes the remainder of this division.

Polynomial.divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative theorem

 {K : Type*} [CommRing K] (f : K[X]) (a : K) : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Full source

theorem divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative
    {K : Type*} [CommRing K] (f : K[X]) (a : K) :
    f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f := by
  have key := by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a
  simpa only [derivative_mul, derivative_sub, derivative_X, derivative_C, sub_zero, one_mul,
    modByMonic_X_sub_C_eq_C_eval] using key

Derivative of Polynomial Division: $\frac{d}{dX}f = q + (X-a) \cdot \frac{d}{dX}q$ where $q = f/(X-a)$

Informal description

Let $K$ be a commutative ring and $f \in K[X]$ be a polynomial. For any $a \in K$, the following equality holds: $$f / (X - a) + (X - a) \cdot \left(\frac{d}{dX}\left(f / (X - a)\right)\right) = \frac{d}{dX}f$$ where $f / (X - a)$ denotes the quotient when $f$ is divided by the monic polynomial $X - a$, and $\frac{d}{dX}$ denotes the formal derivative of a polynomial.

Polynomial.X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic theorem

{K : Type*} [Field K] (f : K[X]) {a : K} (hf : (X - C a) ∣ f /ₘ (X - C a)) : X - C a ∣ derivative f

Full source

theorem X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic {K : Type*} [Field K] (f : K[X]) {a : K}
    (hf : (X - C a) ∣ f /ₘ (X - C a)) : XX - C a ∣ derivative f := by
  have key := divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative f a
  have ⟨u,hu⟩ := hf
  rw [← key, hu, ← mul_add (X - C a) u _]
  use (u + derivative ((X - C a) * u))

Divisibility of Derivative by Linear Factor When Quotient is Divisible

Informal description

Let $K$ be a field and $f \in K[X]$ be a polynomial. For any $a \in K$, if the linear polynomial $X - a$ divides the quotient $f / (X - a)$, then $X - a$ also divides the derivative $f'$ of $f$.

Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero theorem

 {K : Type*} [Field K] (f : K[X]) (a : K) (hf' : f.derivative.eval a ≠ 0) : IsCoprime (X - C a : K[X]) (f /ₘ (X - C a))

Full source

/-- If `f` is a polynomial over a field, and `a : K` satisfies `f' a ≠ 0`,
then `f / (X - a)` is coprime with `X - a`.
Note that we do not assume `f a = 0`, because `f / (X - a) = (f - f a) / (X - a)`. -/
theorem isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type*} [Field K] (f : K[X]) (a : K)
    (hf' : f.derivative.eval a ≠ 0) : IsCoprime (X - C a : K[X]) (f /ₘ (X - C a)) := by
  classical
  refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
  contrapose! hf' with h
  have : XX - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
  rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
  rwa [← C_inj, C_0]

Coprimality of Linear Factor and Quotient When Derivative is Nonzero at Root

Informal description

Let $K$ be a field and $f \in K[X]$ a polynomial. For any element $a \in K$ such that the derivative $f'$ evaluated at $a$ is nonzero (i.e., $f'(a) \neq 0$), the polynomial $X - a$ is coprime with the quotient polynomial $f / (X - a)$ in $K[X]$.

Polynomial.irreducible_iff_degree_lt theorem

 (p : R[X]) (hp0 : p ≠ 0) (hpu : ¬IsUnit p) : Irreducible p ↔ ∀ q, q.degree ≤ ↑(natDegree p / 2) → q ∣ p → IsUnit q

Full source

/-- To check a polynomial over a field is irreducible, it suffices to check only for
divisors that have smaller degree.

See also: `Polynomial.Monic.irreducible_iff_natDegree`.
-/
theorem irreducible_iff_degree_lt (p : R[X]) (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) :
    IrreducibleIrreducible p ↔ ∀ q, q.degree ≤ ↑(natDegree p / 2) → q ∣ p → IsUnit q := by
  rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]
  · simp [hp0, natDegree_mul_leadingCoeff_inv]
  · contrapose! hpu
    exact isUnit_of_mul_eq_one _ _ hpu

Irreducibility Criterion for Polynomials via Degree Bound

Informal description

Let $R$ be a commutative ring and $p \in R[X]$ be a nonzero polynomial that is not a unit. Then $p$ is irreducible if and only if for every polynomial $q \in R[X]$ with $\deg(q) \leq \frac{1}{2}\deg(p)$, if $q$ divides $p$, then $q$ is a unit.

Polynomial.irreducible_iff_lt_natDegree_lt theorem

 {p : R[X]} (hp0 : p ≠ 0) (hpu : ¬IsUnit p) :
  Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬q ∣ p

Full source

/-- To check a polynomial `p` over a field is irreducible, it suffices to check there are no
divisors of degree `0 < d ≤ degree p / 2`.

See also: `Polynomial.Monic.irreducible_iff_natDegree'`.
-/
theorem irreducible_iff_lt_natDegree_lt {p : R[X]} (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) :
    IrreducibleIrreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬ q ∣ p := by
  have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by
    contrapose! hpu
    exact isUnit_of_mul_eq_one _ _ hpu
  rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
      natDegree_mul_leadingCoeff_inv _ hp0]
  simp only [IsUnit.dvd_mul_right
    (isUnit_C.mpr (IsUnit.mk0 (leadingCoeff p)⁻¹ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))]

Irreducibility Criterion for Polynomials via Degree Bounds on Monic Divisors

Informal description

Let $R$ be a commutative ring and $p \in R[X]$ be a nonzero polynomial that is not a unit. Then $p$ is irreducible if and only if for every monic polynomial $q \in R[X]$ with degree $d$ satisfying $0 < d \leq \frac{1}{2}\deg(p)$, the polynomial $q$ does not divide $p$.

Polynomial.leadingCoeff_mul_prod_normalizedFactors theorem

[DecidableEq R] (a : R[X]) : C a.leadingCoeff * (normalizedFactors a).prod = a

Full source

/--
The normalized factors of a polynomial over a field times its leading coefficient give
the polynomial.
-/
theorem leadingCoeff_mul_prod_normalizedFactors [DecidableEq R] (a : R[X]) :
    C a.leadingCoeff * (normalizedFactors a).prod = a := by
  by_cases ha : a = 0
  · simp [ha]
  rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit,
    mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀] <;>
  simp_all

Factorization of Polynomial via Leading Coefficient and Normalized Factors

Informal description

Let $R$ be a field and $a \in R[X]$ be a polynomial. Then the product of the leading coefficient of $a$ (as a constant polynomial) and the product of its normalized factors equals $a$ itself, i.e., \[ C(\text{leadingCoeff}(a)) \cdot \prod_{f \in \text{normalizedFactors}(a)} f = a. \]

Irreducible.natDegree_pos theorem

{F : Type*} [DivisionSemiring F] {f : F[X]} (h : Irreducible f) : 0 < f.natDegree

Full source

/-- An irreducible polynomial over a field must have positive degree. -/
theorem Irreducible.natDegree_pos {F : Type*} [DivisionSemiring F] {f : F[X]} (h : Irreducible f) :
    0 < f.natDegree := Nat.pos_of_ne_zero fun H ↦ by
  obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H
  by_cases hx : x = 0
  · rw [← hf, hx, map_zero] at h; exact not_irreducible_zero h
  exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Irreducible polynomials have positive degree

Informal description

Let $F$ be a division semiring and $f \in F[X]$ be an irreducible polynomial. Then the natural degree of $f$ is positive, i.e., $\mathrm{natDegree}(f) > 0$.