Module docstring
{"# Theory of degrees of polynomials
Some of the main results include
- natDegree_comp_le : The degree of the composition is at most the product of degrees
","Useful lemmas for the \"monicization\" of a nonzero polynomial p. "}
Polynomial.natDegree_comp_le
theorem
: natDegree (p.comp q) ≤ natDegree p * natDegree q
Full source
theorem natDegree_comp_le : natDegree (p.comp q) ≤ natDegree p * natDegree q :=
letI := Classical.decEq R
if h0 : p.comp q = 0 then by rw [h0, natDegree_zero]; exact Nat.zero_le _
else
WithBot.coe_le_coe.1 <|
calc
↑(natDegree (p.comp q)) = degree (p.comp q) := (degree_eq_natDegree h0).symm
_ = _ := congr_arg degree comp_eq_sum_left
_ ≤ _ := degree_sum_le _ _
_ ≤ _ :=
Finset.sup_le fun n hn =>
calc
degree (C (coeff p n) * q ^ n) ≤ degree (C (coeff p n)) + degree (q ^ n) :=
degree_mul_le _ _
_ ≤ natDegree (C (coeff p n)) + n • degree q :=
(add_le_add degree_le_natDegree (degree_pow_le _ _))
_ ≤ natDegree (C (coeff p n)) + n • ↑(natDegree q) :=
(add_le_add_left (nsmul_le_nsmul_right (@degree_le_natDegree _ _ q) n) _)
_ = (n * natDegree q : ℕ) := by
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]
simp
_ ≤ (natDegree p * natDegree q : ℕ) :=
WithBot.coe_le_coe.2 <|
mul_le_mul_of_nonneg_right (le_natDegree_of_ne_zero (mem_support_iff.1 hn))
(Nat.zero_le _)Informal description
For any two polynomials $p$ and $q$ over a semiring $R$, the natural degree of their composition satisfies the inequality:
\[
\deg(p \circ q) \leq \deg(p) \cdot \deg(q).
\]
Polynomial.natDegree_comp_eq_of_mul_ne_zero
theorem
(h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) : natDegree (p.comp q) = natDegree p * natDegree q
Full source
theorem natDegree_comp_eq_of_mul_ne_zero (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) :
natDegree (p.comp q) = natDegree p * natDegree q := by
by_cases hq : natDegree q = 0
· exact le_antisymm natDegree_comp_le (by simp [hq])
apply natDegree_eq_of_le_of_coeff_ne_zero natDegree_comp_le
rwa [coeff_comp_degree_mul_degree hq]Informal description
For any two polynomials $p$ and $q$ over a semiring $R$, if the product of the leading coefficient of $p$ and the leading coefficient of $q$ raised to the power of the natural degree of $p$ is nonzero (i.e., $p_{\deg(p)} \cdot q_{\deg(q)}^{\deg(p)} \neq 0$), then the natural degree of the composition $p \circ q$ is equal to the product of the natural degrees of $p$ and $q$:
\[
\deg(p \circ q) = \deg(p) \cdot \deg(q).
\]
Polynomial.degree_pos_of_root
theorem
{p : R[X]} (hp : p ≠ 0) (h : IsRoot p a) : 0 < degree p
Full source
theorem degree_pos_of_root {p : R[X]} (hp : p ≠ 0) (h : IsRoot p a) : 0 < degree p :=
lt_of_not_ge fun hlt => by
have := eq_C_of_degree_le_zero hlt
rw [IsRoot, this, eval_C] at h
simp only [h, RingHom.map_zero] at this
exact hp thisInformal description
For any nonzero polynomial $p \in R[X]$ over a semiring $R$, if $a$ is a root of $p$ (i.e., $p(a) = 0$), then the degree of $p$ is strictly positive, i.e., $\deg(p) > 0$.
Polynomial.natDegree_le_iff_coeff_eq_zero
theorem
: p.natDegree ≤ n ↔ ∀ N : ℕ, n < N → p.coeff N = 0
Informal description
For a polynomial $p \in R[X]$ and a natural number $n$, the natural degree of $p$ is less than or equal to $n$ if and only if all coefficients of $p$ corresponding to terms of degree greater than $n$ are zero. In other words, $p$ has degree at most $n$ precisely when $p_N = 0$ for all $N > n$, where $p_N$ denotes the coefficient of $X^N$ in $p$.
Polynomial.natDegree_add_le_iff_left
theorem
{n : ℕ} (p q : R[X]) (qn : q.natDegree ≤ n) : (p + q).natDegree ≤ n ↔ p.natDegree ≤ n
Full source
theorem natDegree_add_le_iff_left {n : ℕ} (p q : R[X]) (qn : q.natDegree ≤ n) :
(p + q).natDegree ≤ n ↔ p.natDegree ≤ n := by
refine ⟨fun h => ?_, fun h => natDegree_add_le_of_degree_le h qn⟩
refine natDegree_le_iff_coeff_eq_zero.mpr fun m hm => ?_
convert natDegree_le_iff_coeff_eq_zero.mp h m hm using 1
rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]Informal description
For polynomials $p, q \in R[X]$ over a semiring $R$ and a natural number $n$, if the natural degree of $q$ is at most $n$, then the natural degree of $p + q$ is at most $n$ if and only if the natural degree of $p$ is at most $n$. In other words, given $\mathrm{natDegree}(q) \leq n$, we have:
$$\mathrm{natDegree}(p + q) \leq n \leftrightarrow \mathrm{natDegree}(p) \leq n.$$
Polynomial.natDegree_add_le_iff_right
theorem
{n : ℕ} (p q : R[X]) (pn : p.natDegree ≤ n) : (p + q).natDegree ≤ n ↔ q.natDegree ≤ n
Full source
theorem natDegree_add_le_iff_right {n : ℕ} (p q : R[X]) (pn : p.natDegree ≤ n) :
(p + q).natDegree ≤ n ↔ q.natDegree ≤ n := by
rw [add_comm]
exact natDegree_add_le_iff_left _ _ pnInformal description
For polynomials $p, q \in R[X]$ over a semiring $R$ and a natural number $n$, if the natural degree of $p$ is at most $n$, then the natural degree of $p + q$ is at most $n$ if and only if the natural degree of $q$ is at most $n$. In other words, given $\mathrm{natDegree}(p) \leq n$, we have:
$$\mathrm{natDegree}(p + q) \leq n \leftrightarrow \mathrm{natDegree}(q) \leq n.$$
Polynomial.natDegree_C_mul_le
theorem
(a : R) (f : R[X]) : (C a * f).natDegree ≤ f.natDegree
Full source
theorem natDegree_C_mul_le (a : R) (f : R[X]) : (C a * f).natDegree ≤ f.natDegree := by
simpa using natDegree_mul_le (p := C a)Informal description
For any element $a$ in a semiring $R$ and any polynomial $f \in R[X]$, the natural degree of the product of the constant polynomial $C(a)$ and $f$ satisfies:
\[
\text{natDegree}(C(a) \cdot f) \leq \text{natDegree}(f).
\]
Polynomial.natDegree_mul_C_le
theorem
(f : R[X]) (a : R) : (f * C a).natDegree ≤ f.natDegree
Full source
theorem natDegree_mul_C_le (f : R[X]) (a : R) : (f * C a).natDegree ≤ f.natDegree := by
simpa using natDegree_mul_le (q := C a)Informal description
For any polynomial $f \in R[X]$ over a semiring $R$ and any element $a \in R$, the natural degree of the product $f \cdot C(a)$ is at most the natural degree of $f$, i.e.,
\[
\text{natDegree}(f \cdot C(a)) \leq \text{natDegree}(f).
\]
Polynomial.natDegree_C_mul_eq_of_mul_eq_one
theorem
{ai : R} (au : ai * a = 1) : (C a * p).natDegree = p.natDegree
Full source
theorem natDegree_C_mul_eq_of_mul_eq_one {ai : R} (au : ai * a = 1) :
(C a * p).natDegree = p.natDegree :=
le_antisymm (natDegree_C_mul_le a p)
(calc
p.natDegree = (1 * p).natDegree := by nth_rw 1 [← one_mul p]
_ = (C ai * (C a * p)).natDegree := by rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
_ ≤ (C a * p).natDegree := natDegree_C_mul_le ai (C a * p))Informal description
Let $R$ be a semiring and $a, p \in R[X]$. If there exists an element $a_i \in R$ such that $a_i \cdot a = 1$, then the natural degree of the product of the constant polynomial $C(a)$ and $p$ equals the natural degree of $p$, i.e.,
\[
\text{natDegree}(C(a) \cdot p) = \text{natDegree}(p).
\]
Polynomial.natDegree_mul_C_eq_of_mul_eq_one
theorem
{ai : R} (au : a * ai = 1) : (p * C a).natDegree = p.natDegree
Full source
theorem natDegree_mul_C_eq_of_mul_eq_one {ai : R} (au : a * ai = 1) :
(p * C a).natDegree = p.natDegree :=
le_antisymm (natDegree_mul_C_le p a)
(calc
p.natDegree = (p * 1).natDegree := by nth_rw 1 [← mul_one p]
_ = (p * C a * C ai).natDegree := by rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
_ ≤ (p * C a).natDegree := natDegree_mul_C_le (p * C a) ai)Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any element $a \in R$ with a right inverse $a_i$ (i.e., $a \cdot a_i = 1$), the natural degree of the product $p \cdot C(a)$ equals the natural degree of $p$, i.e.,
\[
\text{natDegree}(p \cdot C(a)) = \text{natDegree}(p).
\]
Polynomial.natDegree_mul_C_eq_of_mul_ne_zero
theorem
(h : p.leadingCoeff * a ≠ 0) : (p * C a).natDegree = p.natDegree
Full source
/-- Although not explicitly stated, the assumptions of lemma `natDegree_mul_C_eq_of_mul_ne_zero`
force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
-/
theorem natDegree_mul_C_eq_of_mul_ne_zero (h : p.leadingCoeff * a ≠ 0) :
(p * C a).natDegree = p.natDegree := by
refine eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_
refine mem_support_iff.mpr ?_
rwa [coeff_mul_C]Informal description
For a polynomial $p \in R[X]$ and an element $a \in R$ such that the product of the leading coefficient of $p$ and $a$ is nonzero, the natural degree of the product $p \cdot C(a)$ equals the natural degree of $p$, i.e.,
\[
\text{natDegree}(p \cdot C(a)) = \text{natDegree}(p).
\]
Polynomial.natDegree_C_mul_of_mul_ne_zero
theorem
(h : a * p.leadingCoeff ≠ 0) : (C a * p).natDegree = p.natDegree
Full source
/-- Although not explicitly stated, the assumptions of lemma `natDegree_C_mul_of_mul_ne_zero`
force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
-/
theorem natDegree_C_mul_of_mul_ne_zero (h : a * p.leadingCoeff ≠ 0) :
(C a * p).natDegree = p.natDegree := by
refine eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) ?_
refine mem_support_iff.mpr ?_
rwa [coeff_C_mul]Informal description
Let $R$ be a semiring, $a \in R$, and $p \in R[X]$ be a nonzero polynomial such that $a \cdot p_{\text{lead}} \neq 0$, where $p_{\text{lead}}$ is the leading coefficient of $p$. Then the natural degree of the product $C(a) \cdot p$ equals the natural degree of $p$, i.e.,
\[
\deg(C(a) \cdot p) = \deg(p).
\]
Polynomial.degree_C_mul_of_mul_ne_zero
theorem
(h : a * p.leadingCoeff ≠ 0) : (C a * p).degree = p.degree
Full source
lemma degree_C_mul_of_mul_ne_zero (h : a * p.leadingCoeff ≠ 0) : (C a * p).degree = p.degree := by
rw [degree_mul' (by simpa)]; simp [left_ne_zero_of_mul h]Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any element $a \in R$ such that $a \cdot \text{lc}(p) \neq 0$ (where $\text{lc}(p)$ is the leading coefficient of $p$), the degree of the product $C(a) \cdot p$ equals the degree of $p$, i.e.,
\[
\deg(C(a) \cdot p) = \deg(p).
\]
Polynomial.natDegree_add_coeff_mul
theorem
(f g : R[X]) : (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
Full source
theorem natDegree_add_coeff_mul (f g : R[X]) :
(f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree := by
simp only [coeff_natDegree, coeff_mul_degree_add_degree]Informal description
For any two polynomials $f$ and $g$ over a semiring $R$, the coefficient of the term $X^{n + m}$ in the product polynomial $f \cdot g$ (where $n = \deg(f)$ and $m = \deg(g)$) is equal to the product of the leading coefficients of $f$ and $g$, i.e.,
$$(f \cdot g)_{n + m} = f_n \cdot g_m.$$
Polynomial.natDegree_lt_coeff_mul
theorem
(h : p.natDegree + q.natDegree < m + n) : (p * q).coeff (m + n) = 0
Full source
theorem natDegree_lt_coeff_mul (h : p.natDegree + q.natDegree < m + n) :
(p * q).coeff (m + n) = 0 :=
coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt h)Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, if the sum of their natural degrees satisfies $\text{natDegree}(p) + \text{natDegree}(q) < m + n$ for some natural numbers $m, n$, then the coefficient of $X^{m+n}$ in the product polynomial $p \cdot q$ is zero, i.e., $(p \cdot q)_{m+n} = 0$.
Polynomial.coeff_mul_of_natDegree_le
theorem
(pm : p.natDegree ≤ m) (qn : q.natDegree ≤ n) : (p * q).coeff (m + n) = p.coeff m * q.coeff n
Full source
theorem coeff_mul_of_natDegree_le (pm : p.natDegree ≤ m) (qn : q.natDegree ≤ n) :
(p * q).coeff (m + n) = p.coeff m * q.coeff n := by
simp_rw [← Polynomial.toFinsupp_apply, toFinsupp_mul]
refine AddMonoidAlgebra.apply_add_of_supDegree_le ?_ Function.injective_id ?_ ?_
· simp
· rwa [supDegree_eq_natDegree, id_eq]
· rwa [supDegree_eq_natDegree, id_eq]Informal description
Let $p$ and $q$ be polynomials over a semiring $R$ such that the natural degree of $p$ is at most $m$ and the natural degree of $q$ is at most $n$. Then the coefficient of the term $X^{m+n}$ in the product polynomial $p \cdot q$ equals the product of the coefficient of $X^m$ in $p$ and the coefficient of $X^n$ in $q$, i.e.,
$$(p \cdot q)_{m+n} = p_m \cdot q_n.$$
Polynomial.coeff_pow_of_natDegree_le
theorem
(pn : p.natDegree ≤ n) : (p ^ m).coeff (m * n) = p.coeff n ^ m
Full source
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
(p ^ m).coeff (m * n) = p.coeff n ^ m := by
induction' m with m hm
· simp
· rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_of_natDegree_le _ pn]
refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
exact mul_le_mul_of_nonneg_left pn m.zero_leInformal description
Let $p$ be a polynomial over a semiring $R$ such that its natural degree satisfies $\text{natDegree}(p) \leq n$. Then for any natural number $m$, the coefficient of $X^{m \cdot n}$ in the polynomial $p^m$ equals the $m$-th power of the coefficient of $X^n$ in $p$, i.e.,
$$(p^m)_{m \cdot n} = (p_n)^m.$$
Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le
theorem
{o : ℕ} (pn : natDegree p ≤ n) (mno : m * n ≤ o) : coeff (p ^ m) o = if o = m * n then (coeff p n) ^ m else 0
Full source
theorem coeff_pow_eq_ite_of_natDegree_le_of_le {o : ℕ}
(pn : natDegree p ≤ n) (mno : m * n ≤ o) :
coeff (p ^ m) o = if o = m * n then (coeff p n) ^ m else 0 := by
rcases eq_or_ne o (m * n) with rfl | h
· simpa only [ite_true] using coeff_pow_of_natDegree_le pn
· simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt <|
lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)Informal description
Let $p$ be a polynomial over a semiring $R$ with $\text{natDegree}(p) \leq n$, and let $m, o \in \mathbb{N}$ such that $m \cdot n \leq o$. Then the coefficient of $X^o$ in $p^m$ is given by:
\[
(p^m)_o = \begin{cases}
(p_n)^m & \text{if } o = m \cdot n, \\
0 & \text{otherwise.}
\end{cases}
\]
Polynomial.coeff_add_eq_left_of_lt
theorem
(qn : q.natDegree < n) : (p + q).coeff n = p.coeff n
Full source
theorem coeff_add_eq_left_of_lt (qn : q.natDegree < n) : (p + q).coeff n = p.coeff n :=
(coeff_add _ _ _).trans <|
(congr_arg _ <| coeff_eq_zero_of_natDegree_lt <| qn).trans <| add_zero _Informal description
For any polynomials $p, q \in R[X]$ and any natural number $n$, if the natural degree of $q$ is strictly less than $n$, then the coefficient of $X^n$ in the sum $p + q$ equals the coefficient of $X^n$ in $p$, i.e.,
$$(p + q)_n = p_n.$$
Polynomial.coeff_add_eq_right_of_lt
theorem
(pn : p.natDegree < n) : (p + q).coeff n = q.coeff n
Full source
theorem coeff_add_eq_right_of_lt (pn : p.natDegree < n) : (p + q).coeff n = q.coeff n := by
rw [add_comm]
exact coeff_add_eq_left_of_lt pnInformal description
For any polynomials $p, q \in R[X]$ and any natural number $n$, if the natural degree of $p$ is strictly less than $n$, then the coefficient of $X^n$ in the sum $p + q$ equals the coefficient of $X^n$ in $q$, i.e.,
$$(p + q)_n = q_n.$$
Polynomial.degree_sum_eq_of_disjoint
theorem
(f : S → R[X]) (s : Finset S) (h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)) :
degree (s.sum f) = s.sup fun i => degree (f i)
Full source
theorem degree_sum_eq_of_disjoint (f : S → R[X]) (s : Finset S)
(h : Set.Pairwise { i | i ∈ s ∧ f i ≠ 0 } (NeNe on degree ∘ f)) :
degree (s.sum f) = s.sup fun i => degree (f i) := by
classical
induction' s using Finset.induction_on with x s hx IH
· simp
· simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
specialize IH (h.mono fun _ => by simp +contextual)
rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
· rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
· rcases s.eq_empty_or_nonempty with (rfl | hs)
· simp
obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
rw [IH, hy'] at H
by_cases hx0 : f x = 0
· simp [hx0, IH]
have hy0 : f y ≠ 0 := by
contrapose! H
simpa [H, degree_eq_bot] using hx0
refine absurd H (h ?_ ?_ fun H => hx ?_)
· simp [hx0]
· simp [hy, hy0]
· exact H.symm ▸ hy
· rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]Informal description
Let $R$ be a semiring and $S$ be a type. Given a finite set $s \subseteq S$ and a function $f : S \to R[X]$ mapping elements of $S$ to polynomials over $R$, suppose that for any two distinct elements $i, j \in s$ with $f(i) \neq 0$ and $f(j) \neq 0$, the degrees of $f(i)$ and $f(j)$ are distinct. Then the degree of the sum $\sum_{i \in s} f(i)$ is equal to the supremum of the degrees of the polynomials $f(i)$ for $i \in s$.
Polynomial.natDegree_sum_eq_of_disjoint
theorem
(f : S → R[X]) (s : Finset S) (h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)) :
natDegree (s.sum f) = s.sup fun i => natDegree (f i)
Full source
theorem natDegree_sum_eq_of_disjoint (f : S → R[X]) (s : Finset S)
(h : Set.Pairwise { i | i ∈ s ∧ f i ≠ 0 } (NeNe on natDegree ∘ f)) :
natDegree (s.sum f) = s.sup fun i => natDegree (f i) := by
by_cases H : ∃ x ∈ s, f x ≠ 0
· obtain ⟨x, hx, hx'⟩ := H
have hs : s.Nonempty := ⟨x, hx⟩
refine natDegree_eq_of_degree_eq_some ?_
rw [degree_sum_eq_of_disjoint]
· rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
Nat.cast_withBot, Finset.coe_sup' hs, ←
Finset.sup'_eq_sup hs]
refine le_antisymm ?_ ?_
· rw [Finset.sup'_le_iff]
intro b hb
by_cases hb' : f b = 0
· simpa [hb'] using hs
rw [degree_eq_natDegree hb', Nat.cast_withBot]
exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
· rw [Finset.sup'_le_iff]
intro b hb
simp only [Finset.le_sup'_iff, exists_prop, Function.comp_apply]
by_cases hb' : f b = 0
· refine ⟨x, hx, ?_⟩
contrapose! hx'
simpa [← Nat.cast_withBot, hb', degree_eq_bot] using hx'
exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
· exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')
· push_neg at H
rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
intro x hx
simp [H x hx]Informal description
Let $R$ be a semiring and $S$ be a type. Given a finite set $s \subseteq S$ and a function $f : S \to R[X]$ mapping elements of $S$ to polynomials over $R$, suppose that for any two distinct elements $i, j \in s$ with $f(i) \neq 0$ and $f(j) \neq 0$, the natural degrees of $f(i)$ and $f(j)$ are distinct. Then the natural degree of the sum $\sum_{i \in s} f(i)$ is equal to the supremum of the natural degrees of the polynomials $f(i)$ for $i \in s$.
Polynomial.natDegree_pos_of_eval₂_root
theorem
{p : R[X]} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : eval₂ f z p = 0) (inj : ∀ x : R, f x = 0 → x = 0) : 0 < natDegree p
Full source
theorem natDegree_pos_of_eval₂_root {p : R[X]} (hp : p ≠ 0) (f : R →+* S) {z : S}
(hz : eval₂ f z p = 0) (inj : ∀ x : R, f x = 0 → x = 0) : 0 < natDegree p :=
lt_of_not_ge fun hlt => by
have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
rw [A, eval₂_C] at hz
simp only [inj (p.coeff 0) hz, RingHom.map_zero] at A
exact hp AInformal description
Let $R$ and $S$ be semirings, and let $p \in R[X]$ be a nonzero polynomial. Given a ring homomorphism $f \colon R \to S$ and an element $z \in S$ such that:
1. The evaluation of $p$ at $z$ via $f$ is zero (i.e., $\text{eval}_2(f, z, p) = 0$), and
2. $f$ is injective (i.e., for any $x \in R$, if $f(x) = 0$ then $x = 0$),
then the natural degree of $p$ is strictly positive (i.e., $\text{natDegree}(p) > 0$).
Polynomial.degree_pos_of_eval₂_root
theorem
{p : R[X]} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : eval₂ f z p = 0) (inj : ∀ x : R, f x = 0 → x = 0) : 0 < degree p
Full source
theorem degree_pos_of_eval₂_root {p : R[X]} (hp : p ≠ 0) (f : R →+* S) {z : S}
(hz : eval₂ f z p = 0) (inj : ∀ x : R, f x = 0 → x = 0) : 0 < degree p :=
natDegree_pos_iff_degree_pos.mp (natDegree_pos_of_eval₂_root hp f hz inj)Informal description
Let $R$ and $S$ be semirings, and let $p \in R[X]$ be a nonzero polynomial. Given a ring homomorphism $f \colon R \to S$ and an element $z \in S$ such that:
1. The evaluation of $p$ at $z$ via $f$ is zero (i.e., $\text{eval}_2(f, z, p) = 0$), and
2. $f$ is injective (i.e., for any $x \in R$, if $f(x) = 0$ then $x = 0$),
then the degree of $p$ is strictly positive (i.e., $\deg(p) > 0$).
Polynomial.coe_lt_degree
theorem
{p : R[X]} {n : ℕ} : (n : WithBot ℕ) < degree p ↔ n < natDegree p
Full source
@[simp]
theorem coe_lt_degree {p : R[X]} {n : ℕ} : (n : WithBot ℕ) < degree p ↔ n < natDegree p := by
by_cases h : p = 0
· simp [h]
simp [degree_eq_natDegree h, Nat.cast_lt]Informal description
For any polynomial $p \in R[X]$ and natural number $n$, the inequality $n < \text{degree}(p)$ holds in $\text{WithBot }\mathbb{N}$ if and only if $n < \text{natDegree}(p)$ holds in $\mathbb{N}$.
Polynomial.degree_map_eq_iff
theorem
{f : R →+* S} {p : Polynomial R} : degree (map f p) = degree p ↔ f (leadingCoeff p) ≠ 0 ∨ p = 0
Full source
@[simp]
theorem degree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
degreedegree (map f p) = degree p ↔ f (leadingCoeff p) ≠ 0 ∨ p = 0 := by
rcases eq_or_ne p 0 with h|h
· simp [h]
simp only [h, or_false]
refine ⟨fun h2 ↦ ?_, degree_map_eq_of_leadingCoeff_ne_zero f⟩
have h3 : natDegree (map f p) = natDegree p := by simp_rw [natDegree, h2]
have h4 : mapmap f p ≠ 0 := by
rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial. The degree of the mapped polynomial $f(p)$ equals the degree of $p$ if and only if either $f$ does not annihilate the leading coefficient of $p$ (i.e., $f(\text{lead}(p)) \neq 0$) or $p$ is the zero polynomial.
Polynomial.natDegree_map_eq_iff
theorem
{f : R →+* S} {p : Polynomial R} : natDegree (map f p) = natDegree p ↔ f (p.leadingCoeff) ≠ 0 ∨ natDegree p = 0
Full source
@[simp]
theorem natDegree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
natDegreenatDegree (map f p) = natDegree p ↔ f (p.leadingCoeff) ≠ 0 ∨ natDegree p = 0 := by
rcases eq_or_ne (natDegree p) 0 with h|h
· simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
have h2 : p ≠ 0 := by rintro rfl; simp at h
simp_all [natDegree, WithBot.unbotD_eq_unbotD_iff]Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial. The natural degree of the mapped polynomial $f(p)$ equals the natural degree of $p$ if and only if either $f$ does not annihilate the leading coefficient of $p$ (i.e., $f(\text{lead}(p)) \neq 0$) or $p$ has degree zero.
Polynomial.natDegree_pos_of_nextCoeff_ne_zero
theorem
(h : p.nextCoeff ≠ 0) : 0 < p.natDegree
Full source
theorem natDegree_pos_of_nextCoeff_ne_zero (h : p.nextCoeff ≠ 0) : 0 < p.natDegree := by
rw [nextCoeff] at h
by_cases hpz : p.natDegree = 0
· simp_all only [ne_eq, zero_le, ite_true, not_true_eq_false]
· apply Nat.zero_lt_of_ne_zero hpzInformal description
For a polynomial $p \in R[X]$, if the next coefficient after the leading coefficient is nonzero (i.e., $p.\text{nextCoeff} \neq 0$), then the natural degree of $p$ is strictly positive (i.e., $0 < p.\text{natDegree}$).
Polynomial.natDegree_sub
theorem
: (p - q).natDegree = (q - p).natDegree
Full source
theorem natDegree_sub : (p - q).natDegree = (q - p).natDegree := by rw [← natDegree_neg, neg_sub]Informal description
For any polynomials $p, q \in R[X]$ over a ring $R$, the natural degree of $p - q$ is equal to the natural degree of $q - p$, i.e., $\text{natDegree}(p - q) = \text{natDegree}(q - p)$.
Polynomial.natDegree_sub_le_iff_left
theorem
(qn : q.natDegree ≤ n) : (p - q).natDegree ≤ n ↔ p.natDegree ≤ n
Full source
theorem natDegree_sub_le_iff_left (qn : q.natDegree ≤ n) :
(p - q).natDegree ≤ n ↔ p.natDegree ≤ n := by
rw [← natDegree_neg] at qn
rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]Informal description
For polynomials $p, q \in R[X]$ over a ring $R$ and a natural number $n$, if the natural degree of $q$ is at most $n$, then the natural degree of $p - q$ is at most $n$ if and only if the natural degree of $p$ is at most $n$. In other words, given $\mathrm{natDegree}(q) \leq n$, we have:
$$\mathrm{natDegree}(p - q) \leq n \leftrightarrow \mathrm{natDegree}(p) \leq n.$$
Polynomial.natDegree_sub_le_iff_right
theorem
(pn : p.natDegree ≤ n) : (p - q).natDegree ≤ n ↔ q.natDegree ≤ n
Full source
theorem natDegree_sub_le_iff_right (pn : p.natDegree ≤ n) :
(p - q).natDegree ≤ n ↔ q.natDegree ≤ n := by rwa [natDegree_sub, natDegree_sub_le_iff_left]Informal description
For polynomials $p, q \in R[X]$ over a ring $R$ and a natural number $n$, if the natural degree of $p$ is at most $n$, then the natural degree of $p - q$ is at most $n$ if and only if the natural degree of $q$ is at most $n$. In other words, given $\mathrm{natDegree}(p) \leq n$, we have:
$$\mathrm{natDegree}(p - q) \leq n \leftrightarrow \mathrm{natDegree}(q) \leq n.$$
Polynomial.coeff_sub_eq_left_of_lt
theorem
(dg : q.natDegree < n) : (p - q).coeff n = p.coeff n
Full source
theorem coeff_sub_eq_left_of_lt (dg : q.natDegree < n) : (p - q).coeff n = p.coeff n := by
rw [← natDegree_neg] at dg
rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]Informal description
For any polynomials $p, q \in R[X]$ over a ring $R$ and any natural number $n$, if the natural degree of $q$ is strictly less than $n$, then the coefficient of $X^n$ in the difference $p - q$ equals the coefficient of $X^n$ in $p$, i.e.,
$$(p - q)_n = p_n.$$
Polynomial.coeff_sub_eq_neg_right_of_lt
theorem
(df : p.natDegree < n) : (p - q).coeff n = -q.coeff n
Full source
theorem coeff_sub_eq_neg_right_of_lt (df : p.natDegree < n) : (p - q).coeff n = -q.coeff n := by
rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]Informal description
For any polynomials $p, q \in R[X]$ over a ring $R$ and any natural number $n$, if the natural degree of $p$ is strictly less than $n$, then the coefficient of $X^n$ in the difference $p - q$ equals the negation of the coefficient of $X^n$ in $q$, i.e.,
$$(p - q)_n = -q_n.$$
Polynomial.nextCoeff_C_mul_X_add_C
theorem
(ha : a ≠ 0) (c : R) : nextCoeff (C a * X + C c) = c
Full source
@[simp]
lemma nextCoeff_C_mul_X_add_C (ha : a ≠ 0) (c : R) : nextCoeff (C a * X + C c) = c := by
rw [nextCoeff_of_natDegree_pos] <;> simp [ha]Informal description
For any nonzero element $a$ in a semiring $R$ and any element $c \in R$, the next coefficient after the leading coefficient in the polynomial $aX + c$ is equal to $c$.
Polynomial.natDegree_eq_one
theorem
: p.natDegree = 1 ↔ ∃ a ≠ 0, ∃ b, C a * X + C b = p
Full source
lemma natDegree_eq_one : p.natDegree = 1 ↔ ∃ a ≠ 0, ∃ b, C a * X + C b = p := by
refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩
· rw [← hp, coeff_natDegree, leadingCoeff_eq_zero] at h
aesop
· ext n
obtain _ | _ | n := n
· simp
· simp
· simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]
rw [coeff_eq_zero_of_natDegree_lt]
simp [hp]
· rintro ⟨a, ha, b, rfl⟩
simp [ha]Informal description
A polynomial $p \in R[X]$ has natural degree $1$ if and only if there exist elements $a, b \in R$ with $a \neq 0$ such that $p = aX + b$.
Polynomial.degree_mul_C
theorem
(a0 : a ≠ 0) : (p * C a).degree = p.degree
Full source
theorem degree_mul_C (a0 : a ≠ 0) : (p * C a).degree = p.degree := by
rw [degree_mul, degree_C a0, add_zero]Informal description
For any nonzero element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the degree of the product $p \cdot C(a)$ is equal to the degree of $p$:
$$\deg(p \cdot C(a)) = \deg(p).$$
Polynomial.degree_C_mul
theorem
(a0 : a ≠ 0) : (C a * p).degree = p.degree
Full source
theorem degree_C_mul (a0 : a ≠ 0) : (C a * p).degree = p.degree := by
rw [degree_mul, degree_C a0, zero_add]Informal description
For any nonzero element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the degree of the product of the constant polynomial $C(a)$ and $p$ is equal to the degree of $p$, i.e.,
$$\deg(a \cdot p) = \deg(p).$$
Polynomial.natDegree_mul_C
theorem
(a0 : a ≠ 0) : (p * C a).natDegree = p.natDegree
Full source
theorem natDegree_mul_C (a0 : a ≠ 0) : (p * C a).natDegree = p.natDegree := by
simp only [natDegree, degree_mul_C a0]Informal description
For any nonzero element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the natural degree of the product $p \cdot C(a)$ is equal to the natural degree of $p$:
$$\text{natDegree}(p \cdot C(a)) = \text{natDegree}(p).$$
Polynomial.natDegree_C_mul
theorem
(a0 : a ≠ 0) : (C a * p).natDegree = p.natDegree
Full source
theorem natDegree_C_mul (a0 : a ≠ 0) : (C a * p).natDegree = p.natDegree := by
simp only [natDegree, degree_C_mul a0]Informal description
For any nonzero element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the natural degree of the product of the constant polynomial $C(a)$ and $p$ is equal to the natural degree of $p$, i.e.,
$$\text{natDegree}(a \cdot p) = \text{natDegree}(p).$$
Polynomial.natDegree_comp
theorem
: natDegree (p.comp q) = natDegree p * natDegree q
Full source
theorem natDegree_comp : natDegree (p.comp q) = natDegree p * natDegree q := by
by_cases q0 : q.natDegree = 0
· rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
natDegree_C, mul_zero]
· by_cases p0 : p = 0
· simp only [p0, zero_comp, natDegree_zero, zero_mul]
· simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]Informal description
For any two polynomials $p$ and $q$ over a semiring $R$, the natural degree of their composition $p \circ q$ is equal to the product of their natural degrees:
\[
\deg(p \circ q) = \deg(p) \cdot \deg(q).
\]
Polynomial.natDegree_iterate_comp
theorem
(k : ℕ) : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
Full source
@[simp]
theorem natDegree_iterate_comp (k : ℕ) :
(p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree := by
induction k with
| zero => simp
| succ k IH => rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]Informal description
For any polynomials $p$ and $q$ over a semiring $R$ and any natural number $k$, the natural degree of the $k$-th iterate of the composition of $p$ with $q$ is given by:
\[
\deg(p \circ^k q) = \deg(p)^k \cdot \deg(q),
\]
where $p \circ^k q$ denotes the $k$-fold composition of $p$ with $q$.
Polynomial.leadingCoeff_comp
theorem
(hq : natDegree q ≠ 0) : leadingCoeff (p.comp q) = leadingCoeff p * leadingCoeff q ^ natDegree p
Full source
theorem leadingCoeff_comp (hq : natDegreenatDegree q ≠ 0) :
leadingCoeff (p.comp q) = leadingCoeff p * leadingCoeff q ^ natDegree p := by
rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]Informal description
For polynomials $p$ and $q$ over a semiring $R$ with no zero divisors, if the natural degree of $q$ is nonzero ($\deg(q) \neq 0$), then the leading coefficient of the composition $p \circ q$ is given by:
\[
\text{lc}(p \circ q) = \text{lc}(p) \cdot \text{lc}(q)^{\deg(p)}.
\]
Polynomial.comp_neg_X_leadingCoeff_eq
theorem
[Ring R] (p : R[X]) : (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff
Full source
@[simp] lemma comp_neg_X_leadingCoeff_eq [Ring R] (p : R[X]) :
(p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff := by
nontriviality R
by_cases h : p = 0
· simp [h]
rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree] <;>
simp [((Commute.neg_one_left _).pow_left _).eq, h]Informal description
For any polynomial $p \in R[X]$ over a ring $R$, the leading coefficient of the composition $p \circ (-X)$ is equal to $(-1)^{\deg(p)}$ times the leading coefficient of $p$, i.e.,
\[
\text{lc}(p(-X)) = (-1)^{\deg(p)} \cdot \text{lc}(p).
\]
Polynomial.comp_eq_zero_iff
theorem
[Semiring R] [NoZeroDivisors R] {p q : R[X]} : p.comp q = 0 ↔ p = 0 ∨ p.eval (q.coeff 0) = 0 ∧ q = C (q.coeff 0)
Full source
lemma comp_eq_zero_iff [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
p.comp q = 0 ↔ p = 0 ∨ p.eval (q.coeff 0) = 0 ∧ q = C (q.coeff 0) := by
refine ⟨fun h ↦ ?_, Or.rec (fun h ↦ by simp [h]) fun h ↦ by rw [h.2, comp_C, h.1, C_0]⟩
have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key
· rw [key, C_comp] at h
exact Or.inl (key.trans h)
· rw [key, comp_C, C_eq_zero] at h
exact Or.inr ⟨h, key⟩Informal description
Let $R$ be a semiring with no zero divisors, and let $p, q \in R[X]$ be polynomials. The composition $p \circ q$ is the zero polynomial if and only if either:
1. $p$ is the zero polynomial, or
2. $p$ evaluates to zero at the constant term of $q$ (i.e., $p(q(0)) = 0$) and $q$ is a constant polynomial (i.e., $q = C(q(0))$).
Polynomial.irreducible_mul_leadingCoeff_inv
theorem
{p : K[X]} : Irreducible (p * C (leadingCoeff p)⁻¹) ↔ Irreducible p
Full source
@[simp]
theorem irreducible_mul_leadingCoeff_inv {p : K[X]} :
IrreducibleIrreducible (p * C (leadingCoeff p)⁻¹) ↔ Irreducible p := by
by_cases hp0 : p = 0
· simp [hp0]
exact irreducible_mul_isUnit
(isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))Informal description
For any nonzero polynomial $p \in K[X]$ over a division ring $K$, the polynomial $p \cdot C(\text{leadingCoeff}(p)^{-1})$ is irreducible if and only if $p$ is irreducible.
Polynomial.dvd_mul_leadingCoeff_inv
theorem
{p q : K[X]} (hp0 : p ≠ 0) : q ∣ p * C (leadingCoeff p)⁻¹ ↔ q ∣ p
Full source
@[simp] lemma dvd_mul_leadingCoeff_inv {p q : K[X]} (hp0 : p ≠ 0) :
q ∣ p * C (leadingCoeff p)⁻¹q ∣ p * C (leadingCoeff p)⁻¹ ↔ q ∣ p :=
IsUnit.dvd_mul_right <| isUnit_C.mpr <| IsUnit.mk0 _ <|
inv_ne_zero <| leadingCoeff_ne_zero.mpr hp0Informal description
Let $K$ be a division ring and $p, q \in K[X]$ be polynomials with $p \neq 0$. Then $q$ divides the product $p \cdot C((\text{leadingCoeff}(p))^{-1})$ if and only if $q$ divides $p$.
Polynomial.monic_mul_leadingCoeff_inv
theorem
{p : K[X]} (h : p ≠ 0) : Monic (p * C (leadingCoeff p)⁻¹)
Full source
theorem monic_mul_leadingCoeff_inv {p : K[X]} (h : p ≠ 0) : Monic (p * C (leadingCoeff p)⁻¹) := by
rw [Monic, leadingCoeff_mul, leadingCoeff_C,
mul_inv_cancel₀ (show leadingCoeffleadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]Informal description
For any nonzero polynomial $p \in K[X]$ over a division ring $K$, the polynomial $p \cdot C((\text{leadingCoeff}(p))^{-1})$ is monic, i.e., its leading coefficient is equal to $1$.
Polynomial.degree_leadingCoeff_inv
theorem
{p : K[X]} (hp0 : p ≠ 0) : degree (C (leadingCoeff p)⁻¹) = 0
Full source
@[simp] lemma degree_leadingCoeff_inv {p : K[X]} (hp0 : p ≠ 0) :
degree (C (leadingCoeff p)⁻¹) = 0 :=
degree_C (inv_ne_zero <| leadingCoeff_ne_zero.mpr hp0)Informal description
For any nonzero polynomial $p \in K[X]$ over a division ring $K$, the degree of the constant polynomial $C((\text{leadingCoeff}(p))^{-1})$ is $0$.
Polynomial.degree_mul_leadingCoeff_inv
theorem
(p : K[X]) {q : K[X]} (h : q ≠ 0) : degree (p * C (leadingCoeff q)⁻¹) = degree p
Full source
theorem degree_mul_leadingCoeff_inv (p : K[X]) {q : K[X]} (h : q ≠ 0) :
degree (p * C (leadingCoeff q)⁻¹) = degree p := by
have h₁ : (leadingCoeff q)⁻¹(leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
rw [degree_mul_C h₁]Informal description
For any polynomial $p \in K[X]$ over a division ring $K$ and any nonzero polynomial $q \in K[X]$, the degree of $p \cdot C((\text{leadingCoeff}(q))^{-1})$ is equal to the degree of $p$, i.e.,
$$\deg(p \cdot C((\text{lc}(q))^{-1})) = \deg(p).$$
Polynomial.natDegree_mul_leadingCoeff_inv
theorem
(p : K[X]) {q : K[X]} (h : q ≠ 0) : natDegree (p * C (leadingCoeff q)⁻¹) = natDegree p
Full source
theorem natDegree_mul_leadingCoeff_inv (p : K[X]) {q : K[X]} (h : q ≠ 0) :
natDegree (p * C (leadingCoeff q)⁻¹) = natDegree p :=
natDegree_eq_of_degree_eq (degree_mul_leadingCoeff_inv _ h)Informal description
For any polynomial $p \in K[X]$ over a division ring $K$ and any nonzero polynomial $q \in K[X]$, the natural degree of $p \cdot C((\text{lc}(q))^{-1})$ is equal to the natural degree of $p$, i.e.,
$$\text{natDegree}(p \cdot C((\text{lc}(q))^{-1})) = \text{natDegree}(p).$$
Polynomial.degree_mul_leadingCoeff_self_inv
theorem
(p : K[X]) : degree (p * C (leadingCoeff p)⁻¹) = degree p
Full source
theorem degree_mul_leadingCoeff_self_inv (p : K[X]) :
degree (p * C (leadingCoeff p)⁻¹) = degree p := by
by_cases hp : p = 0
· simp [hp]
exact degree_mul_leadingCoeff_inv _ hpInformal description
For any polynomial $p \in K[X]$ over a division ring $K$, the degree of $p \cdot C((\text{lc}(p))^{-1})$ is equal to the degree of $p$, i.e.,
$$\deg(p \cdot C((\text{lc}(p))^{-1})) = \deg(p).$$
Polynomial.natDegree_mul_leadingCoeff_self_inv
theorem
(p : K[X]) : natDegree (p * C (leadingCoeff p)⁻¹) = natDegree p
Full source
theorem natDegree_mul_leadingCoeff_self_inv (p : K[X]) :
natDegree (p * C (leadingCoeff p)⁻¹) = natDegree p :=
natDegree_eq_of_degree_eq (degree_mul_leadingCoeff_self_inv _)Informal description
For any polynomial $p$ over a division ring $K$, the natural degree of $p$ multiplied by the constant polynomial $(\text{lc}(p))^{-1}$ is equal to the natural degree of $p$, i.e.,
$$\text{natDegree}(p \cdot C((\text{lc}(p))^{-1})) = \text{natDegree}(p),$$
where $\text{lc}(p)$ denotes the leading coefficient of $p$.
Polynomial.degree_add_degree_leadingCoeff_inv
theorem
(p : K[X]) : degree p + degree (C (leadingCoeff p)⁻¹) = degree p
Full source
@[simp] lemma degree_add_degree_leadingCoeff_inv (p : K[X]) :
degree p + degree (C (leadingCoeff p)⁻¹) = degree p := by
rw [← degree_mul, degree_mul_leadingCoeff_self_inv]Informal description
For any polynomial $p \in K[X]$ over a division ring $K$, the sum of the degrees of $p$ and the constant polynomial $C((\text{lc}(p))^{-1})$ equals the degree of $p$, i.e.,
$$\deg(p) + \deg(C((\text{lc}(p))^{-1})) = \deg(p).$$