Module docstring
{"# Division of univariate polynomials
The main defs are divByMonic and modByMonic.
The compatibility between these is given by modByMonic_add_div.
We also define rootMultiplicity.
"}
Polynomial.X_dvd_iff
theorem
{f : R[X]} : X ∣ f ↔ f.coeff 0 = 0
Informal description
For any polynomial $f$ over a semiring $R$, the polynomial $X$ divides $f$ if and only if the constant term of $f$ (i.e., the coefficient of $X^0$) is zero. In other words, $X \mid f \leftrightarrow f(0) = 0$.
Polynomial.X_pow_dvd_iff
theorem
{f : R[X]} {n : ℕ} : X ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0
Full source
theorem X_pow_dvd_iff {f : R[X]} {n : ℕ} : XX ^ n ∣ fX ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0 :=
⟨fun ⟨g, hgf⟩ d hd => by
simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_lt hd, IsEmpty.forall_iff],
fun hd => by
induction n with
| zero => simp [pow_zero, one_dvd]
| succ n hn =>
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
have := coeff_X_pow_mul g n 0
rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
use k
rwa [pow_succ, mul_assoc, ← hgk]⟩Informal description
For any polynomial $f$ over a semiring $R$ and any natural number $n$, the polynomial $X^n$ divides $f$ if and only if all coefficients of $f$ of degree less than $n$ are zero, i.e., $X^n \mid f \leftrightarrow \forall d < n, f_d = 0$.
Polynomial.finiteMultiplicity_of_degree_pos_of_monic
theorem
(hp : (0 : WithBot ℕ) < degree p) (hmp : Monic p) (hq : q ≠ 0) : FiniteMultiplicity p q
Full source
theorem finiteMultiplicity_of_degree_pos_of_monic (hp : (0 : WithBot ℕ) < degree p) (hmp : Monic p)
(hq : q ≠ 0) : FiniteMultiplicity p q :=
have zn0 : (0 : R) ≠ 1 :=
haveI := Nontrivial.of_polynomial_ne hq
zero_ne_one
⟨natDegree q, fun ⟨r, hr⟩ => by
have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne,
hr0, not_false_eq_true]
have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by
rw [← degree_eq_natDegree hp0]; exact hp
have := congr_arg natDegree hr
rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this
exact
ne_of_lt
(lt_add_of_le_of_pos (le_mul_of_one_le_right (Nat.zero_le _) hnp)
(add_pos_of_pos_of_nonneg (by rwa [one_mul]) (Nat.zero_le _)))
this⟩Informal description
For any nonzero polynomial $q$ and any monic polynomial $p$ with positive degree, the multiplicity of $p$ as a divisor of $q$ is finite. That is, there exists a natural number $n$ such that $p^n$ does not divide $q$.
Polynomial.div_wf_lemma
theorem
(h : degree q ≤ degree p ∧ p ≠ 0) (hq : Monic q) :
degree (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) < degree p
Full source
theorem div_wf_lemma (h : degreedegree q ≤ degree p ∧ p ≠ 0) (hq : Monic q) :
degree (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) < degree p :=
have hp : leadingCoeffleadingCoeff p ≠ 0 := mt leadingCoeff_eq_zero.1 h.2
have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne h.2
have hlt : natDegree q ≤ natDegree p :=
(Nat.cast_le (α := WithBot ℕ)).1
(by rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]; exact h.1)
degree_sub_lt
(by
rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt])
h.2 (by rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C])Informal description
Let $p$ and $q$ be polynomials over a ring $R$ such that $\deg q \leq \deg p$, $p \neq 0$, and $q$ is monic. Then the degree of $p - q \cdot (C(\text{leadingCoeff } p) \cdot X^{\deg p - \deg q})$ is strictly less than the degree of $p$.
Polynomial.divModByMonicAux
definition
: ∀ (_p : R[X]) {q : R[X]}, Monic q → R[X] × R[X]
Full source
/-- See `divByMonic`. -/
noncomputable def divModByMonicAux : ∀ (_p : R[X]) {q : R[X]}, Monic q → R[X]R[X] × R[X]
| p, q, hq =>
letI := Classical.decEq R
if h : degree q ≤ degree p ∧ p ≠ 0 then
let z := C (leadingCoeff p) * X ^ (natDegree p - natDegree q)
have _wf := div_wf_lemma h hq
let dm := divModByMonicAux (p - q * z) hq
⟨z + dm.1, dm.2⟩
else ⟨0, p⟩
termination_by p => pInformal description
Given a polynomial \( p \) and a monic polynomial \( q \), the function returns a pair of polynomials \( (d, m) \) such that \( p = q \cdot d + m \) and \( \deg m < \deg q \). If \( \deg q \leq \deg p \) and \( p \neq 0 \), it recursively computes \( d \) and \( m \) by subtracting \( q \cdot z \) from \( p \), where \( z \) is \( C(\text{leadingCoeff } p) \cdot X^{\deg p - \deg q} \). Otherwise, it returns \( (0, p) \).
Polynomial.divByMonic
definition
(p q : R[X]) : R[X]
Full source
/-- `divByMonic`, denoted as `p /ₘ q`, gives the quotient of `p` by a monic polynomial `q`. -/
def divByMonic (p q : R[X]) : R[X] :=
letI := Classical.decEq R
if hq : Monic q then (divModByMonicAux p hq).1 else 0Informal description
Given polynomials \( p \) and \( q \) over a ring \( R \), the function \( \text{divByMonic} \) computes the quotient of \( p \) divided by \( q \) when \( q \) is monic (i.e., its leading coefficient is 1). If \( q \) is not monic, the function returns the zero polynomial. The division is performed using the auxiliary function \( \text{divModByMonicAux} \), which ensures that the result satisfies the division algorithm properties when \( q \) is monic.
Polynomial.modByMonic
definition
(p q : R[X]) : R[X]
Full source
/-- `modByMonic`, denoted as `p %ₘ q`, gives the remainder of `p` by a monic polynomial `q`. -/
def modByMonic (p q : R[X]) : R[X] :=
letI := Classical.decEq R
if hq : Monic q then (divModByMonicAux p hq).2 else pInformal description
The function `modByMonic`, denoted as `p %ₘ q`, computes the remainder when a polynomial `p` is divided by a monic polynomial `q`. If `q` is not monic, the function returns `p` unchanged.
Polynomial.term_/ₘ_
definition
: Lean.TrailingParserDescr✝
Full source
@[inherit_doc]
infixl:70 " /ₘ " => divByMonicInformal description
The notation `p /ₘ q` represents the division of the polynomial `p` by the monic polynomial `q`, where `divByMonic` is the underlying operation.
Polynomial.term_%ₘ_
definition
: Lean.TrailingParserDescr✝
Full source
@[inherit_doc]
infixl:70 " %ₘ " => modByMonicInformal description
The infix operator `%ₘ` represents the modulo operation for univariate polynomials with respect to a monic polynomial. For polynomials `p` and `q` where `q` is monic, `p %ₘ q` computes the remainder when `p` is divided by `q`.
Polynomial.degree_modByMonic_lt
theorem
[Nontrivial R] : ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), degree (p %ₘ q) < degree q
Full source
theorem degree_modByMonic_lt [Nontrivial R] :
∀ (p : R[X]) {q : R[X]} (_hq : Monic q), degree (p %ₘ q) < degree q
| p, q, hq =>
letI := Classical.decEq R
if h : degree q ≤ degree p ∧ p ≠ 0 then by
have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq
have :=
degree_modByMonic_lt (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
unfold modByMonic at this ⊢
unfold divModByMonicAux
dsimp
rw [dif_pos hq] at this ⊢
rw [if_pos h]
exact this
else
Or.casesOn (not_and_or.1 h)
(by
unfold modByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_neg h]
exact lt_of_not_ge)
(by
intro hp
unfold modByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero)))
termination_by p => pInformal description
Let $R$ be a nontrivial ring. For any polynomial $p \in R[X]$ and any monic polynomial $q \in R[X]$, the degree of the remainder $p \mod q$ is strictly less than the degree of $q$.
Polynomial.natDegree_modByMonic_lt
theorem
(p : R[X]) {q : R[X]} (hmq : Monic q) (hq : q ≠ 1) : natDegree (p %ₘ q) < q.natDegree
Full source
theorem natDegree_modByMonic_lt (p : R[X]) {q : R[X]} (hmq : Monic q) (hq : q ≠ 1) :
natDegree (p %ₘ q) < q.natDegree := by
by_cases hpq : p %ₘ q = 0
· rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero]
contrapose! hq
exact eq_one_of_monic_natDegree_zero hmq hq
· haveI := Nontrivial.of_polynomial_ne hpq
exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)Informal description
Let $R$ be a ring and let $p, q \in R[X]$ be polynomials such that $q$ is monic and $q \neq 1$. Then the degree of the remainder $p \mod q$ is strictly less than the degree of $q$.
Polynomial.zero_modByMonic
theorem
(p : R[X]) : 0 %ₘ p = 0
Full source
@[simp]
theorem zero_modByMonic (p : R[X]) : 0 %ₘ p = 0 := by
classical
unfold modByMonic divModByMonicAux
dsimp
by_cases hp : Monic p
· rw [dif_pos hp, if_neg (mt And.right (not_not_intro rfl)), Prod.snd_zero]
· rw [dif_neg hp]Informal description
For any polynomial $p$ over a ring $R$, the remainder when the zero polynomial is divided by $p$ is zero, i.e., $0 \mod p = 0$.
Polynomial.zero_divByMonic
theorem
(p : R[X]) : 0 /ₘ p = 0
Full source
@[simp]
theorem zero_divByMonic (p : R[X]) : 0 /ₘ p = 0 := by
classical
unfold divByMonic divModByMonicAux
dsimp
by_cases hp : Monic p
· rw [dif_pos hp, if_neg (mt And.right (not_not_intro rfl)), Prod.fst_zero]
· rw [dif_neg hp]Informal description
For any polynomial $p$ over a ring $R$, the division of the zero polynomial by $p$ using the `divByMonic` operation yields the zero polynomial, i.e., $0 /_{\text{monic}} p = 0$.
Polynomial.modByMonic_zero
theorem
(p : R[X]) : p %ₘ 0 = p
Full source
@[simp]
theorem modByMonic_zero (p : R[X]) : p %ₘ 0 = p :=
letI := Classical.decEq R
if h : Monic (0 : R[X]) then by
haveI := monic_zero_iff_subsingleton.mp h
simp [eq_iff_true_of_subsingleton]
else by unfold modByMonic divModByMonicAux; rw [dif_neg h]Informal description
For any polynomial $p$ over a ring $R$, the remainder when $p$ is divided by the zero polynomial is $p$ itself, i.e., $p \mod_{\text{m}} 0 = p$.
Polynomial.divByMonic_zero
theorem
(p : R[X]) : p /ₘ 0 = 0
Full source
@[simp]
theorem divByMonic_zero (p : R[X]) : p /ₘ 0 = 0 :=
letI := Classical.decEq R
if h : Monic (0 : R[X]) then by
haveI := monic_zero_iff_subsingleton.mp h
simp [eq_iff_true_of_subsingleton]
else by unfold divByMonic divModByMonicAux; rw [dif_neg h]Informal description
For any polynomial $p$ over a ring $R$, the quotient of $p$ divided by the zero polynomial is zero, i.e., $p /_{\text{m}} 0 = 0$.
Polynomial.divByMonic_eq_of_not_monic
theorem
(p : R[X]) (hq : ¬Monic q) : p /ₘ q = 0
Full source
theorem divByMonic_eq_of_not_monic (p : R[X]) (hq : ¬Monic q) : p /ₘ q = 0 :=
dif_neg hqInformal description
For any polynomial $p$ over a ring $R$ and any polynomial $q$ that is not monic, the quotient of $p$ divided by $q$ is zero, i.e., $p /_{\text{m}} q = 0$.
Polynomial.modByMonic_eq_of_not_monic
theorem
(p : R[X]) (hq : ¬Monic q) : p %ₘ q = p
Full source
theorem modByMonic_eq_of_not_monic (p : R[X]) (hq : ¬Monic q) : p %ₘ q = p :=
dif_neg hqInformal description
For any polynomial $p$ over a ring $R$ and any polynomial $q$ that is not monic, the remainder of $p$ divided by $q$ is equal to $p$ itself, i.e., $p \mod_{\text{m}} q = p$.
Polynomial.modByMonic_eq_self_iff
theorem
[Nontrivial R] (hq : Monic q) : p %ₘ q = p ↔ degree p < degree q
Full source
theorem modByMonic_eq_self_iff [Nontrivial R] (hq : Monic q) : p %ₘ qp %ₘ q = p ↔ degree p < degree q :=
⟨fun h => h ▸ degree_modByMonic_lt _ hq, fun h => by
classical
have : ¬degree q ≤ degree p := not_le_of_gt h
unfold modByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]⟩Informal description
Let $R$ be a nontrivial ring and $q \in R[X]$ a monic polynomial. For any polynomial $p \in R[X]$, the remainder of $p$ modulo $q$ equals $p$ itself if and only if the degree of $p$ is strictly less than the degree of $q$, i.e.,
\[ p \mod q = p \quad \Leftrightarrow \quad \deg p < \deg q. \]
Polynomial.degree_modByMonic_le
theorem
(p : R[X]) {q : R[X]} (hq : Monic q) : degree (p %ₘ q) ≤ degree q
Full source
theorem degree_modByMonic_le (p : R[X]) {q : R[X]} (hq : Monic q) : degree (p %ₘ q) ≤ degree q := by
nontriviality R
exact (degree_modByMonic_lt _ hq).leInformal description
For any polynomial $p$ over a ring $R$ and any monic polynomial $q \in R[X]$, the degree of the remainder $p \mod_{\text{m}} q$ is less than or equal to the degree of $q$.
Polynomial.degree_modByMonic_le_left
theorem
: degree (p %ₘ q) ≤ degree p
Full source
theorem degree_modByMonic_le_left : degree (p %ₘ q) ≤ degree p := by
nontriviality R
by_cases hq : q.Monic
· cases lt_or_ge (degree p) (degree q)
· rw [(modByMonic_eq_self_iff hq).mpr ‹_›]
· exact (degree_modByMonic_le p hq).trans ‹_›
· rw [modByMonic_eq_of_not_monic p hq]Informal description
For any polynomial $p$ over a ring $R$ and any polynomial $q \in R[X]$, the degree of the remainder $p \mod_{\text{m}} q$ is less than or equal to the degree of $p$, i.e.,
\[ \deg(p \mod_{\text{m}} q) \leq \deg p. \]
Polynomial.natDegree_modByMonic_le
theorem
(p : Polynomial R) {g : Polynomial R} (hg : g.Monic) : natDegree (p %ₘ g) ≤ g.natDegree
Full source
theorem natDegree_modByMonic_le (p : Polynomial R) {g : Polynomial R} (hg : g.Monic) :
natDegree (p %ₘ g) ≤ g.natDegree :=
natDegree_le_natDegree (degree_modByMonic_le p hg)Informal description
For any polynomial $p$ over a ring $R$ and any monic polynomial $g \in R[X]$, the natural degree of the remainder $p \mod_{\text{m}} g$ is less than or equal to the natural degree of $g$.
Polynomial.natDegree_modByMonic_le_left
theorem
: natDegree (p %ₘ q) ≤ natDegree p
Full source
theorem natDegree_modByMonic_le_left : natDegree (p %ₘ q) ≤ natDegree p :=
natDegree_le_natDegree degree_modByMonic_le_leftInformal description
For any polynomial $p$ over a ring $R$ and any polynomial $q \in R[X]$, the natural degree of the remainder $p \mod_{\text{m}} q$ is less than or equal to the natural degree of $p$, i.e.,
\[ \text{natDegree}(p \mod_{\text{m}} q) \leq \text{natDegree}(p). \]
Polynomial.X_dvd_sub_C
theorem
: X ∣ p - C (p.coeff 0)
Full source
theorem X_dvd_sub_C : XX ∣ p - C (p.coeff 0) := by
simp [X_dvd_iff, coeff_C]Informal description
For any polynomial $p$ over a ring $R$, the polynomial $X$ divides $p - C(p(0))$, where $C(p(0))$ is the constant polynomial with value equal to the constant term of $p$.
Polynomial.modByMonic_eq_sub_mul_div
theorem
: ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), p %ₘ q = p - q * (p /ₘ q)
Full source
theorem modByMonic_eq_sub_mul_div :
∀ (p : R[X]) {q : R[X]} (_hq : Monic q), p %ₘ q = p - q * (p /ₘ q)
| p, q, hq =>
letI := Classical.decEq R
if h : degree q ≤ degree p ∧ p ≠ 0 then by
have _wf := div_wf_lemma h hq
have ih := modByMonic_eq_sub_mul_div
(p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
unfold modByMonic divByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_pos h]
rw [modByMonic, dif_pos hq] at ih
refine ih.trans ?_
unfold divByMonic
rw [dif_pos hq, dif_pos hq, if_pos h, mul_add, sub_add_eq_sub_sub]
else by
unfold modByMonic divByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]
termination_by p => pInformal description
For any polynomial $p$ over a ring $R$ and any monic polynomial $q$ over $R$, the remainder of $p$ divided by $q$ equals $p$ minus $q$ multiplied by the quotient of $p$ divided by $q$, i.e.,
\[ p \mod q = p - q \cdot (p / q). \]
Polynomial.modByMonic_add_div
theorem
(p : R[X]) {q : R[X]} (hq : Monic q) : p %ₘ q + q * (p /ₘ q) = p
Full source
theorem modByMonic_add_div (p : R[X]) {q : R[X]} (hq : Monic q) : p %ₘ q + q * (p /ₘ q) = p :=
eq_sub_iff_add_eq.1 (modByMonic_eq_sub_mul_div p hq)Informal description
For any polynomial $p$ over a ring $R$ and any monic polynomial $q$ over $R$, the sum of the remainder $p \mod q$ and the product of $q$ with the quotient $p / q$ equals $p$, i.e.,
\[ p \mod q + q \cdot (p / q) = p. \]
Polynomial.divByMonic_eq_zero_iff
theorem
[Nontrivial R] (hq : Monic q) : p /ₘ q = 0 ↔ degree p < degree q
Full source
theorem divByMonic_eq_zero_iff [Nontrivial R] (hq : Monic q) : p /ₘ qp /ₘ q = 0 ↔ degree p < degree q :=
⟨fun h => by
have := modByMonic_add_div p hq
rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this,
fun h => by
classical
have : ¬degree q ≤ degree p := not_le_of_gt h
unfold divByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]⟩Informal description
Let $R$ be a nontrivial ring and $q \in R[X]$ a monic polynomial. For any polynomial $p \in R[X]$, the quotient $p / q$ obtained by dividing $p$ by $q$ is zero if and only if the degree of $p$ is strictly less than the degree of $q$, i.e.,
\[ p / q = 0 \quad \Leftrightarrow \quad \deg p < \deg q. \]
Polynomial.degree_add_divByMonic
theorem
(hq : Monic q) (h : degree q ≤ degree p) : degree q + degree (p /ₘ q) = degree p
Full source
theorem degree_add_divByMonic (hq : Monic q) (h : degree q ≤ degree p) :
degree q + degree (p /ₘ q) = degree p := by
nontriviality R
have hdiv0 : p /ₘ qp /ₘ q ≠ 0 := by rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]
have hlc : leadingCoeffleadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0 := by
rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
calc
degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
_ ≤ _ := by
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
Nat.cast_add, Nat.cast_le]
exact Nat.le_add_right _ _
calc
degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) := Eq.symm (degree_mul' hlc)
_ = degree (p %ₘ q + q * (p /ₘ q)) := (degree_add_eq_right_of_degree_lt hmod).symm
_ = _ := congr_arg _ (modByMonic_add_div _ hq)Informal description
Let $R$ be a ring and let $q \in R[X]$ be a monic polynomial. For any polynomial $p \in R[X]$ 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_divByMonic_le
theorem
(p q : R[X]) : degree (p /ₘ q) ≤ degree p
Full source
theorem degree_divByMonic_le (p q : R[X]) : degree (p /ₘ q) ≤ degree p :=
letI := Classical.decEq R
if hp0 : p = 0 then by simp only [hp0, zero_divByMonic, le_refl]
else
if hq : Monic q then
if h : degree q ≤ degree p then by
haveI := Nontrivial.of_polynomial_ne hp0
rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)
else by
unfold divByMonic divModByMonicAux
simp [dif_pos hq, h, if_false, degree_zero, bot_le]
else (divByMonic_eq_of_not_monic p hq).symm ▸ bot_leInformal description
For any polynomials $p$ and $q$ over a ring $R$, the degree of the quotient $p / q$ obtained by dividing $p$ by a monic polynomial $q$ is less than or equal to the degree of $p$, i.e.,
\[ \deg(p / q) \leq \deg p. \]
Polynomial.degree_divByMonic_lt
theorem
(p : R[X]) {q : R[X]} (hq : Monic q) (hp0 : p ≠ 0) (h0q : 0 < degree q) : degree (p /ₘ q) < degree p
Full source
theorem degree_divByMonic_lt (p : R[X]) {q : R[X]} (hq : Monic q) (hp0 : p ≠ 0)
(h0q : 0 < degree q) : degree (p /ₘ q) < degree p :=
if hpq : degree p < degree q then by
haveI := Nontrivial.of_polynomial_ne hp0
rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
exact WithBot.bot_lt_coe _
else by
haveI := Nontrivial.of_polynomial_ne hp0
rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
exact
Nat.cast_lt.2
(Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
by simpa [degree_eq_natDegree hq.ne_zero] using h0q))Informal description
Let $R$ be a ring and $p, q \in R[X]$ be polynomials with $q$ monic and $p \neq 0$. If $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.natDegree_divByMonic
theorem
(f : R[X]) {g : R[X]} (hg : g.Monic) : natDegree (f /ₘ g) = natDegree f - natDegree g
Full source
theorem natDegree_divByMonic (f : R[X]) {g : R[X]} (hg : g.Monic) :
natDegree (f /ₘ g) = natDegree f - natDegree g := by
nontriviality R
by_cases hfg : f /ₘ g = 0
· rw [hfg, natDegree_zero]
rw [divByMonic_eq_zero_iff hg] at hfg
rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]
have hgf := hfg
rw [divByMonic_eq_zero_iff hg] at hgf
push_neg at hgf
have := degree_add_divByMonic hg hgf
have hf : f ≠ 0 := by
intro hf
apply hfg
rw [hf, zero_divByMonic]
rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
← Nat.cast_add, Nat.cast_inj] at this
rw [← this, add_tsub_cancel_left]Informal description
Let $R$ be a ring and let $f, g \in R[X]$ be polynomials with $g$ monic. The natural degree of the quotient $f / g$ is equal to the difference between the natural degrees of $f$ and $g$, i.e.,
\[ \text{natDegree}(f / g) = \text{natDegree}(f) - \text{natDegree}(g). \]
Polynomial.div_modByMonic_unique
theorem
{f g} (q r : R[X]) (hg : Monic g) (h : r + g * q = f ∧ degree r < degree g) : f /ₘ g = q ∧ f %ₘ g = r
Full source
theorem div_modByMonic_unique {f g} (q r : R[X]) (hg : Monic g)
(h : r + g * q = f ∧ degree r < degree g) : f /ₘ gf /ₘ g = q ∧ f %ₘ g = r := by
nontriviality R
have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
eq_of_sub_eq_zero
(by
rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f hg).symm)]
simp [mul_add, mul_comm, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])
have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]
have h₄ : degree (r - f %ₘ g) < degree g :=
calc
degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) := degree_sub_le _ _
_ < degree g := max_lt_iff.2 ⟨h.2, degree_modByMonic_lt _ hg⟩
have h₅ : q - f /ₘ g = 0 :=
_root_.by_contradiction fun hqf =>
not_le_of_gt h₄ <|
calc
degree g ≤ degree g + degree (q - f /ₘ g) := by
rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
norm_cast
exact Nat.le_add_right _ _
_ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]
exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩Informal description
Let $f$ and $g$ be polynomials over a ring $R$, with $g$ monic. If polynomials $q$ and $r$ satisfy $r + g \cdot q = f$ and $\deg(r) < \deg(g)$, then $q$ is the quotient and $r$ is the remainder of the division of $f$ by $g$, i.e., $f / g = q$ and $f \mod g = r$.
Polynomial.map_mod_divByMonic
theorem
[Ring S] (f : R →+* S) (hq : Monic q) : (p /ₘ q).map f = p.map f /ₘ q.map f ∧ (p %ₘ q).map f = p.map f %ₘ q.map f
Full source
theorem map_mod_divByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
(p /ₘ q).map f = p.map f /ₘ q.map f ∧ (p %ₘ q).map f = p.map f %ₘ q.map f := by
nontriviality S
haveI : Nontrivial R := f.domain_nontrivial
have : mapmap f p /ₘ map f qmap f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq],
calc
_ ≤ degree (p %ₘ q) := degree_map_le
_ < degree q := degree_modByMonic_lt _ hq
_ = _ :=
Eq.symm <|
degree_map_eq_of_leadingCoeff_ne_zero _
(by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
exact ⟨this.1.symm, this.2.symm⟩Informal description
Let $R$ and $S$ be rings, and let $f : R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$ and any monic polynomial $q \in R[X]$, the following holds:
1. The image under $f$ of the quotient $p / q$ equals the quotient of the images, i.e., $f(p / q) = f(p) / f(q)$.
2. 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.map_divByMonic
theorem
[Ring S] (f : R →+* S) (hq : Monic q) : (p /ₘ q).map f = p.map f /ₘ q.map f
Full source
theorem map_divByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
(p /ₘ q).map f = p.map f /ₘ q.map f :=
(map_mod_divByMonic f hq).1Informal description
Let $R$ and $S$ be rings, and let $f : R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$ and any monic polynomial $q \in R[X]$, the image under $f$ of the quotient $p / q$ equals the quotient of the images, i.e.,
\[ f(p / q) = f(p) / f(q). \]
Polynomial.map_modByMonic
theorem
[Ring S] (f : R →+* S) (hq : Monic q) : (p %ₘ q).map f = p.map f %ₘ q.map f
Full source
theorem map_modByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
(p %ₘ q).map f = p.map f %ₘ q.map f :=
(map_mod_divByMonic f hq).2Informal description
Let $R$ and $S$ be rings, and let $f : R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$ and any monic polynomial $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.modByMonic_eq_zero_iff_dvd
theorem
(hq : Monic q) : p %ₘ q = 0 ↔ q ∣ p
Full source
theorem modByMonic_eq_zero_iff_dvd (hq : Monic q) : p %ₘ qp %ₘ q = 0 ↔ q ∣ p :=
⟨fun h => by rw [← modByMonic_add_div p hq, h, zero_add]; exact dvd_mul_right _ _, fun h => by
nontriviality R
obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h
by_contra hpq0
have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div _ hq, mul_sub, ← hr]
have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
hpq0 <|
leadingCoeff_eq_zero.1
(by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])
have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this
exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.coe_lt_coe.1 this)⟩Informal description
For any polynomial $p$ over a ring $R$ and any monic polynomial $q$ over $R$, the remainder of $p$ divided by $q$ is zero if and only if $q$ divides $p$, i.e.,
\[ p \mod q = 0 \leftrightarrow q \mid p. \]
Polynomial.self_mul_modByMonic
theorem
(hq : q.Monic) : (q * p) %ₘ q = 0
Full source
/-- See `Polynomial.mul_self_modByMonic` for the other multiplication order. That version, unlike
this one, requires commutativity. -/
@[simp]
lemma self_mul_modByMonic (hq : q.Monic) : (q * p) %ₘ q = 0 := by
rw [modByMonic_eq_zero_iff_dvd hq]
exact dvd_mul_right q pInformal description
For any monic polynomial $q$ over a ring $R$ and any polynomial $p$ over $R$, the remainder of the product $q \cdot p$ divided by $q$ is zero, i.e.,
\[ (q \cdot p) \mod q = 0. \]
Polynomial.map_dvd_map
theorem
[Ring S] (f : R →+* S) (hf : Function.Injective f) {x y : R[X]} (hx : x.Monic) : x.map f ∣ y.map f ↔ x ∣ y
Full source
theorem map_dvd_map [Ring S] (f : R →+* S) (hf : Function.Injective f) {x y : R[X]}
(hx : x.Monic) : x.map f ∣ y.map fx.map f ∣ y.map f ↔ x ∣ y := by
rw [← modByMonic_eq_zero_iff_dvd hx, ← modByMonic_eq_zero_iff_dvd (hx.map f), ←
map_modByMonic f hx]
exact
⟨fun H => map_injective f hf <| by rw [H, Polynomial.map_zero], fun H => by
rw [H, Polynomial.map_zero]⟩Informal description
Let $R$ and $S$ be rings, and let $f : R \to S$ be an injective ring homomorphism. For any monic polynomial $x \in R[X]$ and any polynomial $y \in R[X]$, the image polynomial $f(x)$ divides $f(y)$ in $S[X]$ if and only if $x$ divides $y$ in $R[X]$.
Polynomial.modByMonic_one
theorem
(p : R[X]) : p %ₘ 1 = 0
Full source
@[simp]
theorem modByMonic_one (p : R[X]) : p %ₘ 1 = 0 :=
(modByMonic_eq_zero_iff_dvd (by convert monic_one (R := R))).2 (one_dvd _)Informal description
For any polynomial $p$ over a ring $R$, the remainder when $p$ is divided by the monic polynomial $1$ is zero, i.e., $p \mod 1 = 0$.
Polynomial.divByMonic_one
theorem
(p : R[X]) : p /ₘ 1 = p
Full source
@[simp]
theorem divByMonic_one (p : R[X]) : p /ₘ 1 = p := by
conv_rhs => rw [← modByMonic_add_div p monic_one]; simpInformal description
For any polynomial $p$ over a ring $R$, the quotient of $p$ divided by the monic polynomial $1$ is equal to $p$ itself, i.e., $p / 1 = p$.
Polynomial.sum_modByMonic_coeff
theorem
(hq : q.Monic) {n : ℕ} (hn : q.degree ≤ n) : (∑ i : Fin n, monomial i ((p %ₘ q).coeff i)) = p %ₘ q
Full source
theorem sum_modByMonic_coeff (hq : q.Monic) {n : ℕ} (hn : q.degree ≤ n) :
(∑ i : Fin n, monomial i ((p %ₘ q).coeff i)) = p %ₘ q := by
nontriviality R
exact
(sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans
(sum_monomial_eq _)Informal description
Let $R$ be a ring and let $q \in R[X]$ be a monic polynomial. For any polynomial $p \in R[X]$ and any natural number $n$ such that $\deg(q) \leq n$, the sum $\sum_{i < n} X^i \cdot (p \mod q)_i$ equals the remainder $p \mod q$, where $(p \mod q)_i$ denotes the coefficient of $X^i$ in $p \mod q$.
Polynomial.mul_divByMonic_cancel_left
theorem
(p : R[X]) {q : R[X]} (hmo : q.Monic) : q * p /ₘ q = p
Full source
theorem mul_divByMonic_cancel_left (p : R[X]) {q : R[X]} (hmo : q.Monic) :
q * p /ₘ q = p := by
nontriviality R
refine (div_modByMonic_unique _ 0 hmo ⟨by rw [zero_add], ?_⟩).1
rw [degree_zero]
exact Ne.bot_lt fun h => hmo.ne_zero (degree_eq_bot.1 h)Informal description
Let $R$ be a ring and $p, q \in R[X]$ be polynomials with $q$ monic. Then $(q \cdot p) / q = p$, where $/$ denotes division by a monic polynomial.
Polynomial.coeff_divByMonic_X_sub_C_rec
theorem
(p : R[X]) (a : R) (n : ℕ) : (p /ₘ (X - C a)).coeff n = coeff p (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)
Full source
lemma coeff_divByMonic_X_sub_C_rec (p : R[X]) (a : R) (n : ℕ) :
(p /ₘ (X - C a)).coeff n = coeff p (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1) := by
nontriviality R
have := monic_X_sub_C a
set q := p /ₘ (X - C a)
rw [← p.modByMonic_add_div this]
have : degree (p %ₘ (X - C a)) < ↑(n + 1) := degree_X_sub_C a ▸ p.degree_modByMonic_lt this
|>.trans_le <| WithBot.coe_le_coe.mpr le_add_self
simp [q, sub_mul, add_sub, coeff_eq_zero_of_degree_lt this]Informal description
Let $R$ be a ring and $p \in R[X]$ be a polynomial. For any $a \in R$ and $n \in \mathbb{N}$, the coefficient of $X^n$ in the quotient polynomial $p / (X - a)$ (where division is by the monic polynomial $X - a$) satisfies:
\[
\text{coeff}(p / (X - a), n) = \text{coeff}(p, n+1) + a \cdot \text{coeff}(p / (X - a), n+1).
\]
Polynomial.coeff_divByMonic_X_sub_C
theorem
(p : R[X]) (a : R) (n : ℕ) : (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
Full source
theorem coeff_divByMonic_X_sub_C (p : R[X]) (a : R) (n : ℕ) :
(p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i := by
wlog h : p.natDegree ≤ n generalizing n
· refine Nat.decreasingInduction' (fun n hn _ ih ↦ ?_) (le_of_not_le h) ?_
· rw [coeff_divByMonic_X_sub_C_rec, ih, eq_comm, Icc_eq_cons_Ioc (Nat.succ_le.mpr hn),
sum_cons, Nat.sub_self, pow_zero, one_mul, mul_sum]
congr 1; refine sum_congr ?_ fun i hi ↦ ?_
· ext; simp [Nat.succ_le]
rw [← mul_assoc, ← pow_succ', eq_comm, i.sub_succ', Nat.sub_add_cancel]
apply Nat.le_sub_of_add_le
rw [add_comm]; exact (mem_Icc.mp hi).1
· exact this _ le_rfl
rw [Icc_eq_empty (Nat.lt_succ.mpr h).not_le, sum_empty]
nontriviality R
by_cases hp : p.natDegree = 0
· rw [(divByMonic_eq_zero_iff <| monic_X_sub_C a).mpr, coeff_zero]
apply degree_lt_degree; rw [hp, natDegree_X_sub_C]; norm_num
· apply coeff_eq_zero_of_natDegree_lt
rw [natDegree_divByMonic p (monic_X_sub_C a), natDegree_X_sub_C]
exact (Nat.pred_lt hp).trans_le hInformal description
Let $R$ be a ring and $p \in R[X]$ be a polynomial. For any $a \in R$ and $n \in \mathbb{N}$, the coefficient of $X^n$ in the quotient polynomial $p / (X - a)$ (where division is by the monic polynomial $X - a$) is given by:
\[
\text{coeff}(p / (X - a), n) = \sum_{i = n+1}^{\deg p} a^{i - (n+1)} \cdot \text{coeff}(p, i).
\]
Polynomial.not_isField
theorem
: ¬IsField R[X]
Full source
theorem not_isField : ¬IsField R[X] := by
nontriviality R
intro h
letI := h.toField
simpa using congr_arg natDegree (monic_X.eq_one_of_isUnit <| monic_X (R := R).ne_zero.isUnit)Informal description
The ring of univariate polynomials $R[X]$ over a ring $R$ is not a field.
Polynomial.decidableDvdMonic
definition
[DecidableEq R] (p : R[X]) (hq : Monic q) : Decidable (q ∣ p)
Full source
/-- An algorithm for deciding polynomial divisibility.
The algorithm is "compute `p %ₘ q` and compare to `0`".
See `Polynomial.modByMonic` for the algorithm that computes `%ₘ`.
-/
def decidableDvdMonic [DecidableEq R] (p : R[X]) (hq : Monic q) : Decidable (q ∣ p) :=
decidable_of_iff (p %ₘ q = 0) (modByMonic_eq_zero_iff_dvd hq)Informal description
Given a polynomial $p$ over a ring $R$ with decidable equality and a monic polynomial $q$, the function decides whether $q$ divides $p$ by checking if the remainder of $p$ divided by $q$ is zero. This is equivalent to the condition $p \mod q = 0 \leftrightarrow q \mid p$.
Polynomial.finiteMultiplicity_X_sub_C
theorem
(a : R) (h0 : p ≠ 0) : FiniteMultiplicity (X - C a) p
Full source
theorem finiteMultiplicity_X_sub_C (a : R) (h0 : p ≠ 0) : FiniteMultiplicity (X - C a) p := by
haveI := Nontrivial.of_polynomial_ne h0
refine finiteMultiplicity_of_degree_pos_of_monic ?_ (monic_X_sub_C _) h0
rw [degree_X_sub_C]
decideInformal description
For any nonzero polynomial $p$ over a ring $R$ and any element $a \in R$, the multiplicity of $X - a$ as a divisor of $p$ is finite. That is, there exists a natural number $n$ such that $(X - a)^n$ does not divide $p$.
Polynomial.rootMultiplicity
definition
(a : R) (p : R[X]) : ℕ
Full source
/-- The largest power of `X - C a` which divides `p`.
This *could be* computable via the divisibility algorithm `Polynomial.decidableDvdMonic`,
as shown by `Polynomial.rootMultiplicity_eq_nat_find_of_nonzero` which has a computable RHS. -/
def rootMultiplicity (a : R) (p : R[X]) : ℕ :=
letI := Classical.decEq R
if h0 : p = 0 then 0
else
let _ : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
have := decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1))
inferInstanceAs (Decidable ¬_)
Nat.find (finiteMultiplicity_X_sub_C a h0)Informal description
For a polynomial \( p \) over a ring \( R \) and an element \( a \in R \), the root multiplicity of \( a \) in \( p \) is the largest natural number \( n \) such that \( (X - a)^n \) divides \( p \). If \( p = 0 \), the root multiplicity is defined to be 0. This can be computed using the divisibility algorithm for monic polynomials.
Polynomial.rootMultiplicity_eq_nat_find_of_nonzero
theorem
[DecidableEq R] {p : R[X]} (p0 : p ≠ 0) {a : R} :
letI : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
have := decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1))
inferInstanceAs (Decidable ¬_)
rootMultiplicity a p = Nat.find (finiteMultiplicity_X_sub_C a p0)
Full source
theorem rootMultiplicity_eq_nat_find_of_nonzero [DecidableEq R] {p : R[X]} (p0 : p ≠ 0) {a : R} :
letI : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
have := decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1))
inferInstanceAs (Decidable ¬_)
rootMultiplicity a p = Nat.find (finiteMultiplicity_X_sub_C a p0) := by
dsimp [rootMultiplicity]
cases Subsingleton.elim ‹DecidableEq R› (Classical.decEq R)
rw [dif_neg p0]Informal description
Let $R$ be a ring with decidable equality, and let $p \in R[X]$ be a nonzero polynomial. For any element $a \in R$, the root multiplicity of $a$ in $p$ is equal to the smallest natural number $n$ such that $(X - a)^{n+1}$ does not divide $p$. Here, the root multiplicity is defined as the largest $n$ for which $(X - a)^n$ divides $p$.
Polynomial.rootMultiplicity_eq_multiplicity
theorem
[DecidableEq R] (p : R[X]) (a : R) : rootMultiplicity a p = if p = 0 then 0 else multiplicity (X - C a) p
Full source
theorem rootMultiplicity_eq_multiplicity [DecidableEq R]
(p : R[X]) (a : R) :
rootMultiplicity a p =
if p = 0 then 0 else multiplicity (X - C a) p := by
simp only [rootMultiplicity, multiplicity, emultiplicity]
split
· rfl
rename_i h
simp only [finiteMultiplicity_X_sub_C a h, ↓reduceDIte]
rw [← ENat.some_eq_coe, WithTop.untopD_coe]
congrInformal description
For a polynomial $p$ over a ring $R$ with decidable equality and an element $a \in R$, the root multiplicity of $a$ in $p$ is equal to $0$ if $p = 0$, and otherwise it is equal to the multiplicity of the linear polynomial $X - a$ as a divisor of $p$. That is,
\[
\text{rootMultiplicity}(a, p) = \begin{cases}
0 & \text{if } p = 0, \\
\text{multiplicity}(X - a, p) & \text{otherwise.}
\end{cases}
\]
Polynomial.rootMultiplicity_zero
theorem
{x : R} : rootMultiplicity x 0 = 0
Full source
@[simp]
theorem rootMultiplicity_zero {x : R} : rootMultiplicity x 0 = 0 :=
dif_pos rflInformal description
For any element $x$ in a ring $R$, the root multiplicity of $x$ in the zero polynomial is $0$.
Polynomial.rootMultiplicity_C
theorem
(r a : R) : rootMultiplicity a (C r) = 0
Full source
@[simp]
theorem rootMultiplicity_C (r a : R) : rootMultiplicity a (C r) = 0 := by
cases subsingleton_or_nontrivial R
· rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]
classical
rw [rootMultiplicity_eq_multiplicity]
split_ifs with hr
· rfl
have h : natDegree (C r) < natDegree (X - C a) := by simp
simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]Informal description
For any elements $r$ and $a$ in a ring $R$, the root multiplicity of the constant polynomial $C(r)$ at $a$ is zero, i.e., $\text{rootMultiplicity}(a, C(r)) = 0$.
Polynomial.pow_rootMultiplicity_dvd
theorem
(p : R[X]) (a : R) : (X - C a) ^ rootMultiplicity a p ∣ p
Full source
theorem pow_rootMultiplicity_dvd (p : R[X]) (a : R) : (X - C a) ^ rootMultiplicity a p ∣ p :=
letI := Classical.decEq R
if h : p = 0 then by simp [h]
else by
classical
rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvdInformal description
For any polynomial $p$ over a ring $R$ and any element $a \in R$, the polynomial $(X - a)^{\text{rootMultiplicity}(a, p)}$ divides $p$.
Polynomial.pow_mul_divByMonic_rootMultiplicity_eq
theorem
(p : R[X]) (a : R) : (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
Full source
theorem pow_mul_divByMonic_rootMultiplicity_eq (p : R[X]) (a : R) :
(X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p := by
have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
conv_rhs =>
rw [← modByMonic_add_div p this,
(modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]
simpInformal description
For any polynomial $p$ over a ring $R$ and any element $a \in R$, the product of $(X - a)^{\text{rootMultiplicity}(a, p)}$ and the quotient of $p$ divided by $(X - a)^{\text{rootMultiplicity}(a, p)}$ equals $p$, i.e.,
\[ (X - a)^n \cdot (p / (X - a)^n) = p \]
where $n = \text{rootMultiplicity}(a, p)$.
Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd
theorem
(p : R[X]) (hp : p ≠ 0) (a : R) : ∃ q : R[X], p = (X - C a) ^ p.rootMultiplicity a * q ∧ ¬(X - C a) ∣ q
Full source
theorem exists_eq_pow_rootMultiplicity_mul_and_not_dvd (p : R[X]) (hp : p ≠ 0) (a : R) :
∃ q : R[X], p = (X - C a) ^ p.rootMultiplicity a * q ∧ ¬ (X - C a) ∣ q := by
classical
rw [rootMultiplicity_eq_multiplicity, if_neg hp]
apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvdInformal description
For any nonzero polynomial $p$ over a ring $R$ and any element $a \in R$, there exists a polynomial $q$ such that:
\[ p = (X - a)^{\text{rootMultiplicity}(a, p)} \cdot q \]
and $(X - a)$ does not divide $q$.
Polynomial.modByMonic_X_sub_C_eq_C_eval
theorem
(p : R[X]) (a : R) : p %ₘ (X - C a) = C (p.eval a)
Full source
@[simp]
theorem modByMonic_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p %ₘ (X - C a) = C (p.eval a) := by
nontriviality R
have h : (p %ₘ (X - C a)).eval a = p.eval a := by
rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X,
eval_C, sub_self, zero_mul, sub_zero]
have : degree (p %ₘ (X - C a)) < 1 :=
degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
have : degree (p %ₘ (X - C a)) ≤ 0 := by
revert this
cases degree (p %ₘ (X - C a))
· exact fun _ => bot_le
· exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))
rw [eq_C_of_degree_le_zero this, eval_C] at h
rw [eq_C_of_degree_le_zero this, h]Informal description
For any polynomial $p$ over a commutative ring $R$ and any element $a \in R$, the remainder when $p$ is divided by the monic polynomial $X - a$ is equal to the constant polynomial $C(p(a))$, where $p(a)$ denotes the evaluation of $p$ at $a$.
Polynomial.mul_divByMonic_eq_iff_isRoot
theorem
: (X - C a) * (p /ₘ (X - C a)) = p ↔ IsRoot p a
Full source
theorem mul_divByMonic_eq_iff_isRoot : (X - C a) * (p /ₘ (X - C a)) = p ↔ IsRoot p a :=
.trans
⟨fun h => by rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul],
fun h => by
conv_rhs =>
rw [← modByMonic_add_div p (monic_X_sub_C a)]
rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]⟩
IsRoot.def.symmInformal description
For any polynomial $p$ over a commutative ring $R$ and any element $a \in R$, the product of the monic 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(p / (X - a)\right) = p \iff p(a) = 0. \]
Polynomial.dvd_iff_isRoot
theorem
: X - C a ∣ p ↔ IsRoot p a
Informal description
For any polynomial $p$ over a commutative ring $R$ and any element $a \in R$, the linear polynomial $X - a$ divides $p$ if and only if $a$ is a root of $p$ (i.e., $p(a) = 0$). In other words:
\[ X - a \mid p \iff p(a) = 0. \]
Polynomial.X_sub_C_dvd_sub_C_eval
theorem
: X - C a ∣ p - C (p.eval a)
Full source
theorem X_sub_C_dvd_sub_C_eval : XX - C a ∣ p - C (p.eval a) := by
rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]Informal description
For any polynomial $p$ over a commutative ring $R$ and any element $a \in R$, the linear polynomial $X - a$ divides the difference $p - C(p(a))$, where $C(p(a))$ is the constant polynomial with value $p(a)$. In other words:
\[ X - a \mid p - p(a). \]
Polynomial.modByMonic_X
theorem
(p : R[X]) : p %ₘ X = C (p.eval 0)
Full source
theorem modByMonic_X (p : R[X]) : p %ₘ X = C (p.eval 0) := by
rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]Informal description
For any polynomial $p$ over a commutative ring $R$, the remainder when $p$ is divided by the monic polynomial $X$ is equal to the constant polynomial $C(p(0))$, where $p(0)$ denotes the evaluation of $p$ at $0$.
Polynomial.eval₂_modByMonic_eq_self_of_root
theorem
[CommRing S] {f : R →+* S} {p q : R[X]} (hq : q.Monic) {x : S} (hx : q.eval₂ f x = 0) :
(p %ₘ q).eval₂ f x = p.eval₂ f x
Informal description
Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any monic polynomial $q \in R[X]$ and any polynomial $p \in R[X]$, if $x \in S$ is a root of $q$ under the evaluation map $\text{eval}_2 f$ (i.e., $\text{eval}_2 f (q)(x) = 0$), then the evaluation of the remainder $p \mod q$ at $x$ equals the evaluation of $p$ at $x$:
\[ (\text{eval}_2 f) (p \mod q)(x) = (\text{eval}_2 f)(p)(x). \]
Polynomial.sub_dvd_eval_sub
theorem
(a b : R) (p : R[X]) : a - b ∣ p.eval a - p.eval b
Full source
theorem sub_dvd_eval_sub (a b : R) (p : R[X]) : a - b ∣ p.eval a - p.eval b := by
suffices XX - C b ∣ p - C (p.eval b) by
simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this
simp [dvd_iff_isRoot]Informal description
For any elements $a, b$ in a commutative ring $R$ and any polynomial $p \in R[X]$, the difference $a - b$ divides the difference of the evaluations $p(a) - p(b)$.
Polynomial.rootMultiplicity_eq_zero_iff
theorem
{p : R[X]} {x : R} : rootMultiplicity x p = 0 ↔ IsRoot p x → p = 0
Full source
@[simp]
theorem rootMultiplicity_eq_zero_iff {p : R[X]} {x : R} :
rootMultiplicityrootMultiplicity x p = 0 ↔ IsRoot p x → p = 0 := by
classical
simp only [rootMultiplicity_eq_multiplicity, ite_eq_left_iff,
Nat.cast_zero, multiplicity_eq_zero, dvd_iff_isRoot, not_imp_not]Informal description
For a polynomial $p$ over a commutative ring $R$ and an element $x \in R$, the root multiplicity of $x$ in $p$ is zero if and only if the condition that $x$ is a root of $p$ implies that $p$ is the zero polynomial. In other words:
\[
\text{rootMultiplicity}(x, p) = 0 \iff \left( \text{IsRoot}(p, x) \implies p = 0 \right).
\]
Polynomial.rootMultiplicity_eq_zero
theorem
{p : R[X]} {x : R} (h : ¬IsRoot p x) : rootMultiplicity x p = 0
Full source
theorem rootMultiplicity_eq_zero {p : R[X]} {x : R} (h : ¬IsRoot p x) : rootMultiplicity x p = 0 :=
rootMultiplicity_eq_zero_iff.2 fun h' => (h h').elimInformal description
For a polynomial $p$ over a commutative ring $R$ and an element $x \in R$, if $x$ is not a root of $p$ (i.e., $p(x) \neq 0$), then the root multiplicity of $x$ in $p$ is zero.
Polynomial.rootMultiplicity_pos'
theorem
{p : R[X]} {x : R} : 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ IsRoot p x
Full source
@[simp]
theorem rootMultiplicity_pos' {p : R[X]} {x : R} :
0 < rootMultiplicity x p ↔ p ≠ 0 ∧ IsRoot p x := by
rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]Informal description
For a polynomial $p$ over a commutative ring $R$ and an element $x \in R$, the root multiplicity of $x$ in $p$ is positive if and only if $p$ is nonzero and $x$ is a root of $p$. In other words:
\[
\text{rootMultiplicity}(x, p) > 0 \iff p \neq 0 \text{ and } p(x) = 0.
\]
Polynomial.rootMultiplicity_pos
theorem
{p : R[X]} (hp : p ≠ 0) {x : R} : 0 < rootMultiplicity x p ↔ IsRoot p x
Full source
theorem rootMultiplicity_pos {p : R[X]} (hp : p ≠ 0) {x : R} :
0 < rootMultiplicity x p ↔ IsRoot p x :=
rootMultiplicity_pos'.trans (and_iff_right hp)Informal description
For a nonzero polynomial $p$ over a commutative ring $R$ and an element $x \in R$, the root multiplicity of $x$ in $p$ is positive if and only if $x$ is a root of $p$. That is:
\[
\text{rootMultiplicity}(x, p) > 0 \iff p(x) = 0.
\]
Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero
theorem
{p : R[X]} (a : R) (hp : p ≠ 0) : eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0
Full source
theorem eval_divByMonic_pow_rootMultiplicity_ne_zero {p : R[X]} (a : R) (hp : p ≠ 0) :
evaleval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0 := by
classical
haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
rintro ⟨q, hq⟩
have := pow_mul_divByMonic_rootMultiplicity_eq p a
rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
exact
(finiteMultiplicity_of_degree_pos_of_monic
(show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
(monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
(Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)Informal description
For any nonzero polynomial $p$ over a commutative ring $R$ and any element $a \in R$, evaluating the quotient polynomial $p / (X - a)^{\text{rootMultiplicity}(a, p)}$ at $a$ yields a nonzero result. That is,
\[
\left. \frac{p}{(X - a)^n} \right|_{X = a} \neq 0
\]
where $n = \text{rootMultiplicity}(a, p)$ is the largest natural number such that $(X - a)^n$ divides $p$.
Polynomial.mul_self_modByMonic
theorem
(hq : q.Monic) : (p * q) %ₘ q = 0
Full source
/-- See `Polynomial.self_mul_modByMonic` for the other multiplication order. This version, unlike
that one, requires commutativity. -/
@[simp]
lemma mul_self_modByMonic (hq : q.Monic) : (p * q) %ₘ q = 0 := by
rw [modByMonic_eq_zero_iff_dvd hq]
exact dvd_mul_left q pInformal description
For any polynomial $p$ over a commutative ring $R$ and any monic polynomial $q$ over $R$, the remainder of the product $p \cdot q$ divided by $q$ is zero, i.e.,
\[ (p \cdot q) \mod q = 0. \]
Polynomial.modByMonic_eq_of_dvd_sub
theorem
(hq : q.Monic) (h : q ∣ p₁ - p₂) : p₁ %ₘ q = p₂ %ₘ q
Full source
lemma modByMonic_eq_of_dvd_sub (hq : q.Monic) (h : q ∣ p₁ - p₂) : p₁ %ₘ q = p₂ %ₘ q := by
nontriviality R
obtain ⟨f, sub_eq⟩ := h
refine (div_modByMonic_unique (p₂ /ₘ q + f) _ hq ⟨?_, degree_modByMonic_lt _ hq⟩).2
rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div _ hq, add_comm]Informal description
Let $R$ be a commutative ring and let $p_1, p_2, q \in R[X]$ be polynomials with $q$ monic. If $q$ divides $p_1 - p_2$, then the remainders of $p_1$ and $p_2$ modulo $q$ are equal, i.e.,
\[ p_1 \mod q = p_2 \mod q. \]
Polynomial.add_modByMonic
theorem
(p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Full source
lemma add_modByMonic (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + 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 (p₁ /ₘ q + p₂ /ₘ q) _ hq
⟨by
rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div _ hq, ← add_assoc,
add_comm (q * _), modByMonic_add_div _ hq],
(degree_add_le _ _).trans_lt
(max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2
· simp_rw [modByMonic_eq_of_not_monic _ hq]Informal description
For any polynomials $p_1$ and $p_2$ over a commutative ring $R$ and any monic polynomial $q$ over $R$, the remainder of the sum $p_1 + p_2$ divided by $q$ equals the sum of the remainders of $p_1$ and $p_2$ divided by $q$, i.e.,
\[ (p_1 + p_2) \mod q = (p_1 \mod q) + (p_2 \mod q). \]
Polynomial.neg_modByMonic
theorem
(p q : R[X]) : (-p) %ₘ q = -(p %ₘ q)
Full source
lemma neg_modByMonic (p q : R[X]) : (-p) %ₘ q = - (p %ₘ q) := by
rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]Informal description
For any polynomials $p$ and $q$ over a commutative ring $R$, the remainder of the negation of $p$ divided by a monic polynomial $q$ equals the negation of the remainder of $p$ divided by $q$, i.e.,
\[ (-p) \mod q = -(p \mod q). \]
Polynomial.sub_modByMonic
theorem
(p₁ p₂ q : R[X]) : (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q
Full source
lemma sub_modByMonic (p₁ p₂ q : R[X]) : (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q := by
simp [sub_eq_add_neg, add_modByMonic, neg_modByMonic]Informal description
For any polynomials $p_1$, $p_2$, and $q$ over a commutative ring $R$, where $q$ is monic, the remainder of the difference $p_1 - p_2$ divided by $q$ equals the difference of the remainders of $p_1$ and $p_2$ divided by $q$, i.e.,
\[ (p_1 - p_2) \mod q = (p_1 \mod q) - (p_2 \mod q). \]
Polynomial.eval_divByMonic_eq_trailingCoeff_comp
theorem
{p : R[X]} {t : R} : (p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t = (p.comp (X + C t)).trailingCoeff
Full source
lemma eval_divByMonic_eq_trailingCoeff_comp {p : R[X]} {t : R} :
(p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t = (p.comp (X + C t)).trailingCoeff := by
obtain rfl | hp := eq_or_ne p 0
· rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]
have mul_eq := p.pow_mul_divByMonic_rootMultiplicity_eq t
set m := p.rootMultiplicity t
set g := p /ₘ (X - C t) ^ m
have : (g.comp (X + C t)).coeff 0 = g.eval t := by
rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]
rw [← congr_arg (comp · <| X + C t) mul_eq, mul_comp, pow_comp, sub_comp, X_comp, C_comp,
add_sub_cancel_right, ← reverse_leadingCoeff, reverse_X_pow_mul, reverse_leadingCoeff,
trailingCoeff, Nat.le_zero.1 (natTrailingDegree_le_of_ne_zero <|
this ▸ eval_divByMonic_pow_rootMultiplicity_ne_zero t hp), this]Informal description
For any polynomial $p$ over a commutative ring $R$ and any element $t \in R$, the evaluation of the quotient polynomial $p / (X - t)^{\text{rootMultiplicity}(t, p)}$ at $t$ equals the trailing coefficient of the composition $p(X + t)$, i.e.,
\[
\left. \frac{p}{(X - t)^n} \right|_{X = t} = \text{trailingCoeff}(p(X + t))
\]
where $n = \text{rootMultiplicity}(t, p)$.
Polynomial.le_rootMultiplicity_iff
theorem
(p0 : p ≠ 0) {a : R} {n : ℕ} : n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p
Full source
/-- The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff
`(X - a) ^ n` divides `p`. -/
lemma le_rootMultiplicity_iff (p0 : p ≠ 0) {a : R} {n : ℕ} :
n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p := by
classical
rw [rootMultiplicity_eq_nat_find_of_nonzero p0, @Nat.le_find_iff _ (_)]
simp_rw [Classical.not_not]
refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
rcases n with - | n
· rw [pow_zero]
apply one_dvd
· exact h n n.lt_succ_selfInformal description
For a nonzero polynomial $p$ over a commutative ring $R$, an element $a \in R$, and a natural number $n$, the inequality $n \leq \text{rootMultiplicity}(a, p)$ holds if and only if the polynomial $(X - a)^n$ divides $p$.
Polynomial.rootMultiplicity_le_iff
theorem
(p0 : p ≠ 0) (a : R) (n : ℕ) : rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p
Full source
lemma rootMultiplicity_le_iff (p0 : p ≠ 0) (a : R) (n : ℕ) :
rootMultiplicityrootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p := by
rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]Informal description
For a nonzero polynomial $p$ over a commutative ring $R$, an element $a \in R$, and a natural number $n$, the root multiplicity of $a$ in $p$ is at most $n$ if and only if $(X - a)^{n+1}$ does not divide $p$.
Polynomial.rootMultiplicity_add
theorem
{p q : R[X]} (a : R) (hzero : p + q ≠ 0) :
min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)
Full source
/-- The multiplicity of `p + q` is at least the minimum of the multiplicities. -/
lemma rootMultiplicity_add {p q : R[X]} (a : R) (hzero : p + q ≠ 0) :
min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q) := by
rw [le_rootMultiplicity_iff hzero]
exact min_pow_dvd_add (pow_rootMultiplicity_dvd p a) (pow_rootMultiplicity_dvd q a)Informal description
For any polynomials $p$ and $q$ over a commutative ring $R$ and any element $a \in R$, if $p + q \neq 0$, then the root multiplicity of $a$ in $p + q$ is at least the minimum of the root multiplicities of $a$ in $p$ and $q$. That is,
\[ \min(\text{rootMultiplicity}(a, p), \text{rootMultiplicity}(a, q)) \leq \text{rootMultiplicity}(a, p + q). \]
Polynomial.le_rootMultiplicity_mul
theorem
{p q : R[X]} (x : R) (hpq : p * q ≠ 0) : rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)
Full source
lemma le_rootMultiplicity_mul {p q : R[X]} (x : R) (hpq : p * q ≠ 0) :
rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q) := by
rw [le_rootMultiplicity_iff hpq, pow_add]
exact mul_dvd_mul (pow_rootMultiplicity_dvd p x) (pow_rootMultiplicity_dvd q x)Informal description
For any nonzero polynomials $p$ and $q$ over a commutative ring $R$ and any element $x \in R$, the sum of the root multiplicities of $x$ in $p$ and $q$ is less than or equal to the root multiplicity of $x$ in the product $p \cdot q$. That is,
\[ \text{rootMultiplicity}(x, p) + \text{rootMultiplicity}(x, q) \leq \text{rootMultiplicity}(x, p \cdot q). \]
Polynomial.pow_rootMultiplicity_not_dvd
theorem
(p0 : p ≠ 0) (a : R) : ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p
Full source
lemma pow_rootMultiplicity_not_dvd (p0 : p ≠ 0) (a : R) :
¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p := by rw [← rootMultiplicity_le_iff p0]Informal description
For a nonzero polynomial $p$ over a commutative ring $R$ and an element $a \in R$, the polynomial $(X - a)^{n+1}$ does not divide $p$, where $n$ is the root multiplicity of $a$ in $p$.
Polynomial.rootMultiplicity_eq_natTrailingDegree'
theorem
: p.rootMultiplicity 0 = p.natTrailingDegree
Full source
/-- See `Polynomial.rootMultiplicity_eq_natTrailingDegree` for the general case. -/
lemma rootMultiplicity_eq_natTrailingDegree' : p.rootMultiplicity 0 = p.natTrailingDegree := by
by_cases h : p = 0
· simp only [h, rootMultiplicity_zero, natTrailingDegree_zero]
refine le_antisymm ?_ ?_
· rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]
exact ⟨p.natTrailingDegree,
fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt.base _⟩
· rw [le_rootMultiplicity_iff h, map_zero, sub_zero, X_pow_dvd_iff]
exact fun _ ↦ coeff_eq_zero_of_lt_natTrailingDegreeInformal description
For any polynomial $p$ over a commutative ring $R$, the root multiplicity of $0$ in $p$ is equal to the natural trailing degree of $p$, i.e., the smallest natural number $n$ such that the coefficient of $X^n$ in $p$ is nonzero.
Polynomial.leadingCoeff_divByMonic_of_monic
theorem
(hmonic : q.Monic) (hdegree : q.degree ≤ p.degree) : (p /ₘ q).leadingCoeff = p.leadingCoeff
Full source
/-- Division by a monic polynomial doesn't change the leading coefficient. -/
lemma leadingCoeff_divByMonic_of_monic (hmonic : q.Monic)
(hdegree : q.degree ≤ p.degree) : (p /ₘ q).leadingCoeff = p.leadingCoeff := by
nontriviality
have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
Nat.WithBot.one_le_iff_zero_lt] using hdegree
nth_rw 2 [← modByMonic_add_div p hmonic]
rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]
rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]
exact (degree_modByMonic_lt p hmonic).trans_le hdegreeInformal description
Let $R$ be a commutative ring and let $p, q \in R[X]$ be polynomials such that $q$ is monic and $\deg q \leq \deg p$. Then the leading coefficient of the quotient $p / q$ is equal to the leading coefficient of $p$, i.e.,
\[ \text{lc}(p / q) = \text{lc}(p). \]
Polynomial.degree_eq_one_of_irreducible_of_root
theorem
(hi : Irreducible p) {x : R} (hx : IsRoot p x) : degree p = 1
Full source
lemma degree_eq_one_of_irreducible_of_root (hi : Irreducible p) {x : R} (hx : IsRoot p x) :
degree p = 1 :=
let ⟨g, hg⟩ := dvd_iff_isRoot.2 hx
have : IsUnitIsUnit (X - C x) ∨ IsUnit g := hi.isUnit_or_isUnit hg
this.elim
(fun h => by
have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h
rw [h₁] at h₂; exact absurd h₂ (by decide))
fun hgu => by rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]Informal description
Let $R$ be a commutative ring and let $p \in R[X]$ be an irreducible polynomial. If $x \in R$ is a root of $p$ (i.e., $p(x) = 0$), then the degree of $p$ is equal to $1$.
Polynomial.leadingCoeff_divByMonic_X_sub_C
theorem
(p : R[X]) (hp : degree p ≠ 0) (a : R) : leadingCoeff (p /ₘ (X - C a)) = leadingCoeff p
Full source
lemma leadingCoeff_divByMonic_X_sub_C (p : R[X]) (hp : degreedegree p ≠ 0) (a : R) :
leadingCoeff (p /ₘ (X - C a)) = leadingCoeff p := by
nontriviality
rcases hp.lt_or_lt with hd | hd
· rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]
refine leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) ?_
rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]Informal description
Let $R$ be a commutative ring and $p \in R[X]$ be a non-constant polynomial (i.e., $\deg p \neq 0$). For any $a \in R$, the leading coefficient of the quotient $p / (X - a)$ is equal to the leading coefficient of $p$, i.e.,
\[ \text{lc}(p / (X - a)) = \text{lc}(p). \]
Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff
theorem
{p q : R[X]} (hpq : p ∣ q) (h₁ : q.natDegree ≤ p.natDegree) (h₂ : q.leadingCoeff ∣ p.leadingCoeff) : Associated p q
Full source
lemma associated_of_dvd_of_natDegree_le_of_leadingCoeff {p q : R[X]} (hpq : p ∣ q)
(h₁ : q.natDegree ≤ p.natDegree) (h₂ : q.leadingCoeff ∣ p.leadingCoeff) :
Associated p q :=
have ⟨r, hr⟩ := hpq
have ⟨u, hu⟩ := associated_of_dvd_dvd ⟨leadingCoeff r, hr ▸ leadingCoeff_mul p r⟩ h₂
⟨Units.map C.toMonoidHom u, eq_of_dvd_of_natDegree_le_of_leadingCoeff
(by rwa [Units.mul_right_dvd]) (by simpa [natDegree_mul_C] using h₁) (by simpa using hu)⟩Informal description
Let $R$ be a commutative ring and let $p, q \in R[X]$ be polynomials such that:
1. $p$ divides $q$ (denoted $p \mid q$),
2. The degree of $q$ is less than or equal to the degree of $p$,
3. The leading coefficient of $q$ divides the leading coefficient of $p$.
Then $p$ and $q$ are *associated*, i.e., there exists a unit $u \in R^\times$ such that $p = u \cdot q$.
Polynomial.associated_of_dvd_of_natDegree_le
theorem
{K} [Field K] {p q : K[X]} (hpq : p ∣ q) (hq : q ≠ 0) (h₁ : q.natDegree ≤ p.natDegree) : Associated p q
Full source
lemma associated_of_dvd_of_natDegree_le {K} [Field K] {p q : K[X]} (hpq : p ∣ q) (hq : q ≠ 0)
(h₁ : q.natDegree ≤ p.natDegree) : Associated p q :=
associated_of_dvd_of_natDegree_le_of_leadingCoeff hpq h₁
(IsUnit.dvd (by rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq))Informal description
Let $K$ be a field and let $p, q \in K[X]$ be polynomials such that:
1. $p$ divides $q$ (i.e., $p \mid q$),
2. $q$ is nonzero,
3. The degree of $q$ is less than or equal to the degree of $p$.
Then $p$ and $q$ are *associated*, meaning there exists a unit $u \in K^\times$ such that $p = u \cdot q$.
Polynomial.associated_of_dvd_of_degree_eq
theorem
{K} [Field K] {p q : K[X]} (hpq : p ∣ q) (h₁ : p.degree = q.degree) : Associated p q
Full source
lemma associated_of_dvd_of_degree_eq {K} [Field K] {p q : K[X]} (hpq : p ∣ q)
(h₁ : p.degree = q.degree) : Associated p q :=
(Classical.em (q = 0)).elim (fun hq ↦ (show p = q by simpa [hq] using h₁) ▸ Associated.refl p)
(associated_of_dvd_of_natDegree_le hpq · (natDegree_le_natDegree h₁.ge))Informal description
Let $K$ be a field and let $p, q \in K[X]$ be polynomials such that:
1. $p$ divides $q$ (i.e., $p \mid q$),
2. The degree of $p$ is equal to the degree of $q$.
Then $p$ and $q$ are *associated*, meaning there exists a unit $u \in K^\times$ such that $p = u \cdot q$.