doc-next-gen

Mathlib.Algebra.Polynomial.Degree.Operations

Module docstring

{"# Lemmas for calculating the degree of univariate polynomials

Main results

  • degree_mul : The degree of the product is the sum of degrees
  • leadingCoeff_add_of_degree_eq and leadingCoeff_add_of_degree_lt : The leading coefficient of a sum is determined by the leading coefficients and degrees "}
Polynomial.supDegree_eq_degree theorem
(p : R[X]) : p.toFinsupp.supDegree WithBot.some = p.degree
Full source 
theorem supDegree_eq_degree (p : R[X]) : p.toFinsupp.supDegree WithBot.some = p.degree :=
  max_eq_sup_coe
Supremum Degree of Polynomial Finsupp Equals Polynomial Degree
Informal description
For any univariate polynomial $p \in R[X]$ over a semiring $R$, the supremum degree of its associated finsupp (viewed in `WithBot ℕ`) coincides with the polynomial's degree. That is, $\text{supDegree}(\text{toFinsupp}(p)) = \text{degree}(p)$.
Polynomial.degree_lt_wf theorem
: WellFounded fun p q : R[X] => degree p < degree q
Full source 
theorem degree_lt_wf : WellFounded fun p q : R[X] => degree p < degree q :=
  InvImage.wf degree wellFounded_lt
Well-foundedness of the Degree Ordering on Polynomials
Informal description
The relation defined by `degree p < degree q` on the space of univariate polynomials `R[X]` is well-founded.
Polynomial.instWellFoundedRelation instance
: WellFoundedRelation R[X]
Full source 
instance : WellFoundedRelation R[X] :=
  ⟨_, degree_lt_wf⟩
Well-founded Degree Ordering on Polynomials
Informal description
The space of univariate polynomials $R[X]$ over a semiring $R$ has a well-founded relation given by the degree ordering.
Polynomial.monic_of_subsingleton theorem
[Subsingleton R] (p : R[X]) : Monic p
Full source 
@[nontriviality]
theorem monic_of_subsingleton [Subsingleton R] (p : R[X]) : Monic p :=
  Subsingleton.elim _ _
Polynomials over a subsingleton semiring are monic
Informal description
For any univariate polynomial $p$ over a semiring $R$ where $R$ is a subsingleton (i.e., all elements of $R$ are equal), $p$ is monic (i.e., its leading coefficient is 1).
Polynomial.degree_of_subsingleton theorem
[Subsingleton R] : degree p = ⊥
Full source 
@[nontriviality]
theorem degree_of_subsingleton [Subsingleton R] : degree p = ⊥ := by
  rw [Subsingleton.elim p 0, degree_zero]
Degree of Polynomial over Subsingleton Semiring is Bottom
Informal description
For any univariate polynomial $p$ over a semiring $R$ where $R$ is a subsingleton (i.e., all elements of $R$ are equal), the degree of $p$ is the bottom element $\bot$ (representing "no degree").
Polynomial.natDegree_of_subsingleton theorem
[Subsingleton R] : natDegree p = 0
Full source 
@[nontriviality]
theorem natDegree_of_subsingleton [Subsingleton R] : natDegree p = 0 := by
  rw [Subsingleton.elim p 0, natDegree_zero]
Degree Zero for Polynomials over Subsingleton Semirings
Informal description
For any univariate polynomial $p$ over a subsingleton semiring $R$ (where all elements of $R$ are equal), the degree of $p$ as a natural number is $0$.
Polynomial.le_natDegree_of_ne_zero theorem
(h : coeff p n ≠ 0) : n ≤ natDegree p
Full source 
theorem le_natDegree_of_ne_zero (h : coeffcoeff p n ≠ 0) : n ≤ natDegree p := by
  rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]
  · exact le_degree_of_ne_zero h
  · rintro rfl
    exact h rfl
Coefficient Nonzero Implies Degree Bound: $p_n \neq 0 \Rightarrow n \leq \deg(p)$
Informal description
For a univariate polynomial $p$ over a semiring $R$, if the coefficient of $X^n$ in $p$ is nonzero, then $n$ is less than or equal to the degree of $p$, i.e., $n \leq \deg(p)$.
Polynomial.degree_eq_of_le_of_coeff_ne_zero theorem
(pn : p.degree ≤ n) (p1 : p.coeff n ≠ 0) : p.degree = n
Full source 
theorem degree_eq_of_le_of_coeff_ne_zero (pn : p.degree ≤ n) (p1 : p.coeff n ≠ 0) : p.degree = n :=
  pn.antisymm (le_degree_of_ne_zero p1)
Degree Equality Condition for Polynomials: $\deg(p) \leq n$ and $p_n \neq 0$ implies $\deg(p) = n$
Informal description
For a univariate polynomial $p$ over a semiring $R$, if the degree of $p$ is at most $n$ and the coefficient of $X^n$ in $p$ is nonzero, then the degree of $p$ is exactly $n$.
Polynomial.natDegree_eq_of_le_of_coeff_ne_zero theorem
(pn : p.natDegree ≤ n) (p1 : p.coeff n ≠ 0) : p.natDegree = n
Full source 
theorem natDegree_eq_of_le_of_coeff_ne_zero (pn : p.natDegree ≤ n) (p1 : p.coeff n ≠ 0) :
    p.natDegree = n :=
  pn.antisymm (le_natDegree_of_ne_zero p1)
Natural Degree Characterization: $\text{natDegree}(p) \leq n$ and $p_n \neq 0$ implies $\text{natDegree}(p) = n$
Informal description
For a univariate polynomial $p$ over a semiring $R$, if the natural degree of $p$ is at most $n$ (i.e., $\text{natDegree}(p) \leq n$) and the coefficient of $X^n$ in $p$ is nonzero (i.e., $p_n \neq 0$), then the natural degree of $p$ is exactly $n$ (i.e., $\text{natDegree}(p) = n$).
Polynomial.natDegree_lt_natDegree theorem
{q : S[X]} (hp : p ≠ 0) (hpq : p.degree < q.degree) : p.natDegree < q.natDegree
Full source 
theorem natDegree_lt_natDegree {q : S[X]} (hp : p ≠ 0) (hpq : p.degree < q.degree) :
    p.natDegree < q.natDegree := by
  by_cases hq : q = 0
  · exact (not_lt_bot <| hq ▸ hpq).elim
  rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq
Natural Degree Strict Inequality for Polynomials: $\deg(p) < \deg(q) \implies \text{natDegree}(p) < \text{natDegree}(q)$
Informal description
For any nonzero univariate polynomial $p$ and any polynomial $q$ over a semiring $S$, if the degree of $p$ is strictly less than the degree of $q$, then the natural degree of $p$ is strictly less than the natural degree of $q$.
Polynomial.natDegree_eq_natDegree theorem
{q : S[X]} (hpq : p.degree = q.degree) : p.natDegree = q.natDegree
Full source 
lemma natDegree_eq_natDegree {q : S[X]} (hpq : p.degree = q.degree) :
    p.natDegree = q.natDegree := by simp [natDegree, hpq]
Equality of Natural Degrees for Polynomials with Equal Degrees
Informal description
For two univariate polynomials $p$ and $q$ over a semiring $S$, if their degrees are equal (i.e., $\deg(p) = \deg(q)$), then their natural degrees are also equal (i.e., $\text{natDegree}(p) = \text{natDegree}(q)$).
Polynomial.coeff_eq_zero_of_degree_lt theorem
(h : degree p < n) : coeff p n = 0
Full source 
theorem coeff_eq_zero_of_degree_lt (h : degree p < n) : coeff p n = 0 :=
  Classical.not_not.1 (mt le_degree_of_ne_zero (not_le_of_gt h))
Vanishing of Coefficients Beyond Degree: $\deg(p) < n \implies p_n = 0$
Informal description
For any univariate polynomial $p$ over a semiring and any natural number $n$, if the degree of $p$ is strictly less than $n$, then the coefficient of $X^n$ in $p$ is zero.
Polynomial.coeff_eq_zero_of_natDegree_lt theorem
{p : R[X]} {n : ℕ} (h : p.natDegree < n) : p.coeff n = 0
Full source 
theorem coeff_eq_zero_of_natDegree_lt {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
    p.coeff n = 0 := by
  apply coeff_eq_zero_of_degree_lt
  by_cases hp : p = 0
  · subst hp
    exact WithBot.bot_lt_coe n
  · rwa [degree_eq_natDegree hp, Nat.cast_lt]
Vanishing of Coefficients Beyond Natural Degree: $\text{natDegree}(p) < n \implies p_n = 0$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, if the natural degree of $p$ is strictly less than $n$, then the coefficient of $X^n$ in $p$ is zero.
Polynomial.ext_iff_natDegree_le theorem
{p q : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) : p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
Full source 
theorem ext_iff_natDegree_le {p q : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) :
    p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i := by
  refine Iff.trans Polynomial.ext_iff ?_
  refine forall_congr' fun i => ⟨fun h _ => h, fun h => ?_⟩
  refine (le_or_lt i n).elim h fun k => ?_
  exact
    (coeff_eq_zero_of_natDegree_lt (hp.trans_lt k)).trans
      (coeff_eq_zero_of_natDegree_lt (hq.trans_lt k)).symm
Polynomial Equality via Coefficient Equality up to Natural Degree $n$
Informal description
For two univariate polynomials $p$ and $q$ over a semiring $R$ and a natural number $n$, if both $p$ and $q$ have natural degree at most $n$, then $p = q$ if and only if their coefficients are equal for all terms of degree at most $n$. That is, under the conditions $\text{natDegree}(p) \leq n$ and $\text{natDegree}(q) \leq n$, we have: $$ p = q \leftrightarrow \forall i \leq n, \text{coeff}(p, i) = \text{coeff}(q, i). $$
Polynomial.ext_iff_degree_le theorem
{p q : R[X]} {n : ℕ} (hp : p.degree ≤ n) (hq : q.degree ≤ n) : p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
Full source 
theorem ext_iff_degree_le {p q : R[X]} {n : ℕ} (hp : p.degree ≤ n) (hq : q.degree ≤ n) :
    p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i :=
  ext_iff_natDegree_le (natDegree_le_of_degree_le hp) (natDegree_le_of_degree_le hq)
Polynomial Equality via Coefficient Equality up to Degree $n$
Informal description
For two univariate polynomials $p$ and $q$ over a semiring $R$ and a natural number $n$, if both $p$ and $q$ have degree at most $n$, then $p = q$ if and only if their coefficients are equal for all terms of degree at most $n$. That is, under the conditions $\deg(p) \leq n$ and $\deg(q) \leq n$, we have: $$ p = q \leftrightarrow \forall i \leq n, \text{coeff}(p, i) = \text{coeff}(q, i). $$
Polynomial.coeff_natDegree_succ_eq_zero theorem
{p : R[X]} : p.coeff (p.natDegree + 1) = 0
Full source 
@[simp]
theorem coeff_natDegree_succ_eq_zero {p : R[X]} : p.coeff (p.natDegree + 1) = 0 :=
  coeff_eq_zero_of_natDegree_lt (lt_add_one _)
Vanishing of Coefficient Beyond Natural Degree: $p_{n+1} = 0$ where $n = \text{natDegree}(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$, the coefficient of the term $X^{n+1}$ in $p$ is zero, where $n$ is the natural degree of $p$. In other words, $p_{n+1} = 0$ where $n = \text{natDegree}(p)$.
Polynomial.ite_le_natDegree_coeff theorem
(p : R[X]) (n : ℕ) (I : Decidable (n < 1 + natDegree p)) : @ite _ (n < 1 + natDegree p) I (coeff p n) 0 = coeff p n
Full source 
theorem ite_le_natDegree_coeff (p : R[X]) (n : ℕ) (I : Decidable (n < 1 + natDegree p)) :
    @ite _ (n < 1 + natDegree p) I (coeff p n) 0 = coeff p n := by
  split_ifs with h
  · rfl
  · exact (coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm
Coefficient Extraction via Conditional: $\text{coeff}(p, n) = \text{ite}(n < 1 + \text{natDegree}(p), \text{coeff}(p, n), 0)$
Informal description
For any polynomial $p$ over a semiring $R$ and any natural number $n$, the coefficient of $X^n$ in $p$ is equal to the conditional expression that returns $\text{coeff}(p, n)$ if $n < 1 + \text{natDegree}(p)$ and $0$ otherwise. In other words, $\text{coeff}(p, n) = \begin{cases} \text{coeff}(p, n) & \text{if } n < 1 + \text{natDegree}(p) \\ 0 & \text{otherwise} \end{cases}$.
Polynomial.coeff_mul_X_sub_C theorem
{p : R[X]} {r : R} {a : ℕ} : coeff (p * (X - C r)) (a + 1) = coeff p a - coeff p (a + 1) * r
Full source 
theorem coeff_mul_X_sub_C {p : R[X]} {r : R} {a : ℕ} :
    coeff (p * (X - C r)) (a + 1) = coeff p a - coeff p (a + 1) * r := by simp [mul_sub]
Coefficient Formula for Polynomial Multiplication by $(X - r)$: $[X^{a+1}](p \cdot (X - r)) = p_a - p_{a+1} \cdot r$
Informal description
For any polynomial $p \in R[X]$, element $r \in R$, and natural number $a \in \mathbb{N}$, the coefficient of $X^{a+1}$ in the product $p \cdot (X - r)$ is equal to the difference between the coefficient of $X^a$ in $p$ and the product of the coefficient of $X^{a+1}$ in $p$ with $r$, i.e., $$[X^{a+1}](p \cdot (X - r)) = p_a - p_{a+1} \cdot r.$$
Polynomial.coeff_natDegree_eq_zero_of_degree_lt theorem
(h : degree p < degree q) : coeff p (natDegree q) = 0
Full source 
theorem coeff_natDegree_eq_zero_of_degree_lt (h : degree p < degree q) :
    coeff p (natDegree q) = 0 :=
  coeff_eq_zero_of_degree_lt (lt_of_lt_of_le h degree_le_natDegree)
Vanishing of Polynomial Coefficient at Higher Degree: $\deg(p) < \deg(q) \implies p_{\deg(q)} = 0$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the degree of $p$ is strictly less than the degree of $q$, then the coefficient of $p$ corresponding to the degree of $q$ is zero. In other words, if $\deg(p) < \deg(q)$, then $p_{\deg(q)} = 0$.
Polynomial.ne_zero_of_degree_gt theorem
{n : WithBot ℕ} (h : n < degree p) : p ≠ 0
Full source 
theorem ne_zero_of_degree_gt {n : WithBot ℕ} (h : n < degree p) : p ≠ 0 :=
  mt degree_eq_bot.2 h.ne_bot
Nonzero Polynomial When Degree Exceeds Given Bound
Informal description
For any univariate polynomial $p$ over a semiring and any extended natural number $n$ (including $\bot$), if $n$ is strictly less than the degree of $p$, then $p$ is not the zero polynomial.
Polynomial.ne_zero_of_degree_ge_degree theorem
(hpq : p.degree ≤ q.degree) (hp : p ≠ 0) : q ≠ 0
Full source 
theorem ne_zero_of_degree_ge_degree (hpq : p.degree ≤ q.degree) (hp : p ≠ 0) : q ≠ 0 :=
  Polynomial.ne_zero_of_degree_gt
    (lt_of_lt_of_le (bot_lt_iff_ne_bot.mpr (by rwa [Ne, Polynomial.degree_eq_bot])) hpq :
      q.degree > ⊥)
Nonzero Polynomial Implication via Degree Comparison: $\deg(p) \leq \deg(q) \land p \neq 0 \implies q \neq 0$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the degree of $p$ is less than or equal to the degree of $q$ and $p$ is not the zero polynomial, then $q$ is not the zero polynomial.
Polynomial.ne_zero_of_natDegree_gt theorem
{n : ℕ} (h : n < natDegree p) : p ≠ 0
Full source 
theorem ne_zero_of_natDegree_gt {n : ℕ} (h : n < natDegree p) : p ≠ 0 := fun H => by
  simp [H, Nat.not_lt_zero] at h
Nonzero Polynomial Has Degree Greater Than Any Natural Number Less Than Its Degree
Informal description
For any natural number $n$ and any nonzero polynomial $p$ over a semiring $R$, if $n$ is less than the degree of $p$, then $p$ is not the zero polynomial.
Polynomial.degree_lt_degree theorem
(h : natDegree p < natDegree q) : degree p < degree q
Full source 
theorem degree_lt_degree (h : natDegree p < natDegree q) : degree p < degree q := by
  by_cases hp : p = 0
  · simp only [hp, degree_zero]
    rw [bot_lt_iff_ne_bot]
    intro hq
    simp [hp, degree_eq_bot.mp hq, lt_irrefl] at h
  · rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]
Natural Degree Comparison Implies Degree Comparison for Polynomials: $\deg_{\mathbb{N}}(p) < \deg_{\mathbb{N}}(q) \implies \deg(p) < \deg(q)$
Informal description
For any nonzero polynomials $p$ and $q$ over a semiring, if the natural degree of $p$ is strictly less than the natural degree of $q$, then the degree of $p$ is strictly less than the degree of $q$.
Polynomial.natDegree_lt_natDegree_iff theorem
(hp : p ≠ 0) : natDegree p < natDegree q ↔ degree p < degree q
Full source 
theorem natDegree_lt_natDegree_iff (hp : p ≠ 0) : natDegreenatDegree p < natDegree q ↔ degree p < degree q :=
  ⟨degree_lt_degree, fun h ↦ by
    have hq : q ≠ 0 := ne_zero_of_degree_gt h
    rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h⟩
Equivalence of Natural Degree and Degree Comparisons for Polynomials: $\deg_{\mathbb{N}}(p) < \deg_{\mathbb{N}}(q) \Leftrightarrow \deg(p) < \deg(q)$
Informal description
For any nonzero polynomial $p$ over a semiring, the natural degree of $p$ is strictly less than the natural degree of another polynomial $q$ if and only if the degree of $p$ is strictly less than the degree of $q$. In other words, $\deg_{\mathbb{N}}(p) < \deg_{\mathbb{N}}(q) \Leftrightarrow \deg(p) < \deg(q)$.
Polynomial.degree_le_zero_iff theorem
: degree p ≤ 0 ↔ p = C (coeff p 0)
Full source 
theorem degree_le_zero_iff : degreedegree p ≤ 0 ↔ p = C (coeff p 0) :=
  ⟨eq_C_of_degree_le_zero, fun h => h.symm ▸ degree_C_le⟩
Degree Bound for Constant Polynomials: $\deg(p) \leq 0 \leftrightarrow p = C(p(0))$
Informal description
For any univariate polynomial $p$ over a semiring $R$, the degree of $p$ is less than or equal to $0$ if and only if $p$ is equal to the constant polynomial whose coefficient is the constant term of $p$, i.e., $\deg(p) \leq 0 \leftrightarrow p = C(p(0))$.
Polynomial.degree_add_eq_left_of_degree_lt theorem
(h : degree q < degree p) : degree (p + q) = degree p
Full source 
theorem degree_add_eq_left_of_degree_lt (h : degree q < degree p) : degree (p + q) = degree p :=
  le_antisymm (max_eq_left_of_lt h ▸ degree_add_le _ _) <|
    degree_le_degree <| by
      rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]
      exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)
Degree of Sum When Second Term Has Lower Degree: $\deg(p + q) = \deg(p)$ if $\deg(q) < \deg(p)$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the degree of $q$ is strictly less than the degree of $p$, then the degree of the sum $p + q$ is equal to the degree of $p$, i.e., $\deg(p + q) = \deg(p)$.
Polynomial.degree_add_eq_right_of_degree_lt theorem
(h : degree p < degree q) : degree (p + q) = degree q
Full source 
theorem degree_add_eq_right_of_degree_lt (h : degree p < degree q) : degree (p + q) = degree q := by
  rw [add_comm, degree_add_eq_left_of_degree_lt h]
Degree of Sum When First Term Has Lower Degree: $\deg(p + q) = \deg(q)$ if $\deg(p) < \deg(q)$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the degree of $p$ is strictly less than the degree of $q$, then the degree of the sum $p + q$ is equal to the degree of $q$, i.e., $\deg(p + q) = \deg(q)$.
Polynomial.natDegree_add_eq_left_of_degree_lt theorem
(h : degree q < degree p) : natDegree (p + q) = natDegree p
Full source 
theorem natDegree_add_eq_left_of_degree_lt (h : degree q < degree p) :
    natDegree (p + q) = natDegree p :=
  natDegree_eq_of_degree_eq (degree_add_eq_left_of_degree_lt h)
Natural Degree of Sum When Second Term Has Lower Degree: $\text{natDegree}(p + q) = \text{natDegree}(p)$ if $\deg(q) < \deg(p)$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the degree of $q$ is strictly less than the degree of $p$, then the natural degree of the sum $p + q$ is equal to the natural degree of $p$, i.e., $\text{natDegree}(p + q) = \text{natDegree}(p)$.
Polynomial.natDegree_add_eq_left_of_natDegree_lt theorem
(h : natDegree q < natDegree p) : natDegree (p + q) = natDegree p
Full source 
theorem natDegree_add_eq_left_of_natDegree_lt (h : natDegree q < natDegree p) :
    natDegree (p + q) = natDegree p :=
  natDegree_add_eq_left_of_degree_lt (degree_lt_degree h)
Natural Degree of Sum When Second Term Has Lower Natural Degree: $\text{natDegree}(p + q) = \text{natDegree}(p)$ if $\text{natDegree}(q) < \text{natDegree}(p)$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the natural degree of $q$ is strictly less than the natural degree of $p$, then the natural degree of the sum $p + q$ is equal to the natural degree of $p$, i.e., $\text{natDegree}(p + q) = \text{natDegree}(p)$.
Polynomial.natDegree_add_eq_right_of_degree_lt theorem
(h : degree p < degree q) : natDegree (p + q) = natDegree q
Full source 
theorem natDegree_add_eq_right_of_degree_lt (h : degree p < degree q) :
    natDegree (p + q) = natDegree q :=
  natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h)
Natural Degree of Sum When First Term Has Lower Degree: $\text{natDegree}(p + q) = \text{natDegree}(q)$ if $\deg(p) < \deg(q)$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the degree of $p$ is strictly less than the degree of $q$, then the natural degree of the sum $p + q$ is equal to the natural degree of $q$, i.e., $\text{natDegree}(p + q) = \text{natDegree}(q)$.
Polynomial.natDegree_add_eq_right_of_natDegree_lt theorem
(h : natDegree p < natDegree q) : natDegree (p + q) = natDegree q
Full source 
theorem natDegree_add_eq_right_of_natDegree_lt (h : natDegree p < natDegree q) :
    natDegree (p + q) = natDegree q :=
  natDegree_add_eq_right_of_degree_lt (degree_lt_degree h)
Natural Degree of Sum When First Term Has Lower Natural Degree
Informal description
For any univariate polynomials $p$ and $q$ over a semiring, if the natural degree of $p$ is strictly less than the natural degree of $q$, then the natural degree of the sum $p + q$ is equal to the natural degree of $q$, i.e., $\text{natDegree}(p + q) = \text{natDegree}(q)$.
Polynomial.degree_add_C theorem
(hp : 0 < degree p) : degree (p + C a) = degree p
Full source 
theorem degree_add_C (hp : 0 < degree p) : degree (p + C a) = degree p :=
  add_comm (C a) p ▸ degree_add_eq_right_of_degree_lt <| lt_of_le_of_lt degree_C_le hp
Degree Preservation Under Constant Addition: $\deg(p + C(a)) = \deg(p)$ for $\deg(p) > 0$
Informal description
For any univariate polynomial $p$ over a semiring $R$ with positive degree and any constant $a \in R$, the degree of the sum $p + C(a)$ equals the degree of $p$, i.e., $\deg(p + C(a)) = \deg(p)$.
Polynomial.natDegree_add_C theorem
{a : R} : (p + C a).natDegree = p.natDegree
Full source 
@[simp] theorem natDegree_add_C {a : R} : (p + C a).natDegree = p.natDegree := by
  rcases eq_or_ne p 0 with rfl | hp
  · simp
  by_cases hpd : p.degree ≤ 0
  · rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]
  · rw [not_le, degree_eq_natDegree hp, Nat.cast_pos, ← natDegree_C a] at hpd
    exact natDegree_add_eq_left_of_natDegree_lt hpd
Natural Degree Invariance Under Constant Addition: $\text{natDegree}(p + C(a)) = \text{natDegree}(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any constant $a \in R$, the natural degree of the sum $p + C(a)$ equals the natural degree of $p$, i.e., $\text{natDegree}(p + C(a)) = \text{natDegree}(p)$.
Polynomial.natDegree_C_add theorem
{a : R} : (C a + p).natDegree = p.natDegree
Full source 
@[simp] theorem natDegree_C_add {a : R} : (C a + p).natDegree = p.natDegree := by
  simp [add_comm _ p]
Natural Degree Invariance Under Left Constant Addition: $\text{natDegree}(C(a) + p) = \text{natDegree}(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any constant $a \in R$, the natural degree of the sum $C(a) + p$ equals the natural degree of $p$, i.e., $\text{natDegree}(C(a) + p) = \text{natDegree}(p)$.
Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero theorem
(h : leadingCoeff p + leadingCoeff q ≠ 0) : degree (p + q) = max p.degree q.degree
Full source 
theorem degree_add_eq_of_leadingCoeff_add_ne_zero (h : leadingCoeffleadingCoeff p + leadingCoeff q ≠ 0) :
    degree (p + q) = max p.degree q.degree :=
  le_antisymm (degree_add_le _ _) <|
    match lt_trichotomy (degree p) (degree q) with
    | Or.inl hlt => by
      rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]
    | Or.inr (Or.inl HEq) =>
      le_of_not_gt fun hlt : max (degree p) (degree q) > degree (p + q) =>
        h <|
          show leadingCoeff p + leadingCoeff q = 0 by
            rw [HEq, max_self] at hlt
            rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]
            exact coeff_natDegree_eq_zero_of_degree_lt hlt
    | Or.inr (Or.inr hlt) => by
      rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]
Degree of Sum When Leading Coefficients Add to Nonzero: $\deg(p + q) = \max(\deg p, \deg q)$
Informal description
For univariate polynomials $p$ and $q$ over a semiring, if the sum of their leading coefficients is nonzero, then the degree of their sum equals the maximum of their degrees, i.e., $$\deg(p + q) = \max(\deg p, \deg q).$$
Polynomial.natDegree_eq_of_natDegree_add_lt_left theorem
(p q : R[X]) (H : natDegree (p + q) < natDegree p) : natDegree p = natDegree q
Full source 
lemma natDegree_eq_of_natDegree_add_lt_left (p q : R[X])
    (H : natDegree (p + q) < natDegree p) : natDegree p = natDegree q := by
  by_contra h
  cases Nat.lt_or_lt_of_ne h with
  | inl h => exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)
  | inr h =>
    rw [natDegree_add_eq_left_of_natDegree_lt h] at H
    exact LT.lt.false H
Natural Degree Equality from Sum Having Lower Degree Than First Term: $\text{natDegree}(p + q) < \text{natDegree}(p) \implies \text{natDegree}(p) = \text{natDegree}(q)$
Informal description
For univariate polynomials $p$ and $q$ over a semiring, if the natural degree of their sum is strictly less than the natural degree of $p$, then the natural degrees of $p$ and $q$ are equal, i.e., $\text{natDegree}(p) = \text{natDegree}(q)$.
Polynomial.natDegree_eq_of_natDegree_add_lt_right theorem
(p q : R[X]) (H : natDegree (p + q) < natDegree q) : natDegree p = natDegree q
Full source 
lemma natDegree_eq_of_natDegree_add_lt_right (p q : R[X])
    (H : natDegree (p + q) < natDegree q) : natDegree p = natDegree q :=
  (natDegree_eq_of_natDegree_add_lt_left q p (add_comm p q ▸ H)).symm
Natural Degree Equality from Sum Having Lower Degree Than Second Term: $\text{natDegree}(p + q) < \text{natDegree}(q) \implies \text{natDegree}(p) = \text{natDegree}(q)$
Informal description
For univariate polynomials $p$ and $q$ over a semiring $R$, if the natural degree of their sum is strictly less than the natural degree of $q$, then the natural degrees of $p$ and $q$ are equal, i.e., $\text{natDegree}(p) = \text{natDegree}(q)$.
Polynomial.natDegree_eq_of_natDegree_add_eq_zero theorem
(p q : R[X]) (H : natDegree (p + q) = 0) : natDegree p = natDegree q
Full source 
lemma natDegree_eq_of_natDegree_add_eq_zero (p q : R[X])
    (H : natDegree (p + q) = 0) : natDegree p = natDegree q := by
  by_cases h₁ : natDegree p = 0; on_goal 1 => by_cases h₂ : natDegree q = 0
  · exact h₁.trans h₂.symm
  · apply natDegree_eq_of_natDegree_add_lt_right; rwa [H, Nat.pos_iff_ne_zero]
  · apply natDegree_eq_of_natDegree_add_lt_left; rwa [H, Nat.pos_iff_ne_zero]
Natural Degree Equality from Zero-Degree Sum: $\text{natDegree}(p + q) = 0 \implies \text{natDegree}(p) = \text{natDegree}(q)$
Informal description
For univariate polynomials $p$ and $q$ over a semiring $R$, if the natural degree of their sum is zero, then the natural degrees of $p$ and $q$ are equal, i.e., $\text{natDegree}(p) = \text{natDegree}(q)$.
Polynomial.monic_of_natDegree_le_of_coeff_eq_one theorem
(n : ℕ) (pn : p.natDegree ≤ n) (p1 : p.coeff n = 1) : Monic p
Full source 
theorem monic_of_natDegree_le_of_coeff_eq_one (n : ℕ) (pn : p.natDegree ≤ n) (p1 : p.coeff n = 1) :
    Monic p := by
  unfold Monic
  nontriviality
  refine (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn ?_).trans p1
  exact ne_of_eq_of_ne p1 one_ne_zero
Monic Polynomial Characterization via Degree and Leading Coefficient
Informal description
For a univariate polynomial $p$ over a semiring $R$ and a natural number $n$, if the natural degree of $p$ is at most $n$ (i.e., $\text{natDegree}(p) \leq n$) and the coefficient of $X^n$ in $p$ is $1$ (i.e., $p_n = 1$), then $p$ is monic.
Polynomial.monic_of_degree_le_of_coeff_eq_one theorem
(n : ℕ) (pn : p.degree ≤ n) (p1 : p.coeff n = 1) : Monic p
Full source 
theorem monic_of_degree_le_of_coeff_eq_one (n : ℕ) (pn : p.degree ≤ n) (p1 : p.coeff n = 1) :
    Monic p :=
  monic_of_natDegree_le_of_coeff_eq_one n (natDegree_le_of_degree_le pn) p1
Monic polynomial criterion via degree and leading coefficient
Informal description
Let $p$ be a univariate polynomial over a semiring $R$ and let $n$ be a natural number. If the degree of $p$ is at most $n$ (i.e., $\deg(p) \leq n$) and the coefficient of $X^n$ in $p$ is $1$ (i.e., $p_n = 1$), then $p$ is monic.
Polynomial.leadingCoeff_add_of_degree_lt theorem
(h : degree p < degree q) : leadingCoeff (p + q) = leadingCoeff q
Full source 
theorem leadingCoeff_add_of_degree_lt (h : degree p < degree q) :
    leadingCoeff (p + q) = leadingCoeff q := by
  have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h
  simp only [leadingCoeff, natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h), this,
    coeff_add, zero_add]
Leading Coefficient of Sum When First Polynomial Has Lower Degree: $\text{lc}(p + q) = \text{lc}(q)$ if $\deg(p) < \deg(q)$
Informal description
For univariate polynomials $p$ and $q$ over a semiring $R$, if the degree of $p$ is strictly less than the degree of $q$, then the leading coefficient of their sum $p + q$ equals the leading coefficient of $q$, i.e., $$\text{lc}(p + q) = \text{lc}(q).$$
Polynomial.leadingCoeff_add_of_degree_lt' theorem
(h : degree q < degree p) : leadingCoeff (p + q) = leadingCoeff p
Full source 
theorem leadingCoeff_add_of_degree_lt' (h : degree q < degree p) :
    leadingCoeff (p + q) = leadingCoeff p := by
  rw [add_comm]
  exact leadingCoeff_add_of_degree_lt h
Leading Coefficient of Sum When Second Polynomial Has Lower Degree: $\text{lc}(p + q) = \text{lc}(p)$ if $\deg(q) < \deg(p)$
Informal description
For univariate polynomials $p$ and $q$ over a semiring $R$, if the degree of $q$ is strictly less than the degree of $p$, then the leading coefficient of their sum $p + q$ equals the leading coefficient of $p$, i.e., $$\text{lc}(p + q) = \text{lc}(p).$$
Polynomial.leadingCoeff_add_of_degree_eq theorem
(h : degree p = degree q) (hlc : leadingCoeff p + leadingCoeff q ≠ 0) : leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q
Full source 
theorem leadingCoeff_add_of_degree_eq (h : degree p = degree q)
    (hlc : leadingCoeffleadingCoeff p + leadingCoeff q ≠ 0) :
    leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q := by
  have : natDegree (p + q) = natDegree p := by
    apply natDegree_eq_of_degree_eq
    rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
  simp only [leadingCoeff, this, natDegree_eq_of_degree_eq h, coeff_add]
Leading Coefficient of Sum When Degrees Are Equal and Leading Coefficients Sum to Nonzero
Informal description
For univariate polynomials $p$ and $q$ over a semiring $R$, if $p$ and $q$ have the same degree and the sum of their leading coefficients is nonzero, then the leading coefficient of their sum $p + q$ equals the sum of their leading coefficients, i.e., $$\text{lc}(p + q) = \text{lc}(p) + \text{lc}(q).$$
Polynomial.coeff_mul_degree_add_degree theorem
(p q : R[X]) : coeff (p * q) (natDegree p + natDegree q) = leadingCoeff p * leadingCoeff q
Full source 
@[simp]
theorem coeff_mul_degree_add_degree (p q : R[X]) :
    coeff (p * q) (natDegree p + natDegree q) = leadingCoeff p * leadingCoeff q :=
  calc
    coeff (p * q) (natDegree p + natDegree q) =
        ∑ x ∈ antidiagonal (natDegree p + natDegree q), coeff p x.1 * coeff q x.2 :=
      coeff_mul _ _ _
    _ = coeff p (natDegree p) * coeff q (natDegree q) := by
      refine Finset.sum_eq_single (natDegree p, natDegree q) ?_ ?_
      · rintro ⟨i, j⟩ h₁ h₂
        rw [mem_antidiagonal] at h₁
        by_cases H : natDegree p < i
        · rw [coeff_eq_zero_of_degree_lt
              (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),
            zero_mul]
        · rw [not_lt_iff_eq_or_lt] at H
          rcases H with H | H
          · subst H
            rw [add_left_cancel_iff] at h₁
            dsimp at h₁
            subst h₁
            exact (h₂ rfl).elim
          · suffices natDegree q < j by
              rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]
            by_contra! H'
            exact
              ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
                h₁
      · intro H
        exfalso
        apply H
        rw [mem_antidiagonal]
Coefficient of Highest Degree Term in Polynomial Product: $(p \cdot q)_{n + m} = \text{lc}(p) \cdot \text{lc}(q)$
Informal description
For any two univariate polynomials $p$ and $q$ over a semiring $R$, the coefficient of the term $X^{n + m}$ in the product $p \cdot q$ (where $n = \deg(p)$ and $m = \deg(q)$) is equal to the product of the leading coefficients of $p$ and $q$, i.e., $$(p \cdot q)_{n + m} = \text{lc}(p) \cdot \text{lc}(q).$$
Polynomial.degree_mul' theorem
(h : leadingCoeff p * leadingCoeff q ≠ 0) : degree (p * q) = degree p + degree q
Full source 
theorem degree_mul' (h : leadingCoeffleadingCoeff p * leadingCoeff q ≠ 0) :
    degree (p * q) = degree p + degree q :=
  have hp : p ≠ 0 := by refine mt ?_ h; exact fun hp => by rw [hp, leadingCoeff_zero, zero_mul]
  have hq : q ≠ 0 := by refine mt ?_ h; exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]
  le_antisymm (degree_mul_le _ _)
    (by
      rw [degree_eq_natDegree hp, degree_eq_natDegree hq]
      refine le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_
      rwa [coeff_mul_degree_add_degree])
Degree of Polynomial Product: $\deg(p \cdot q) = \deg(p) + \deg(q)$ when $\text{lc}(p)\text{lc}(q) \neq 0$
Informal description
For any two univariate polynomials $p$ and $q$ over a semiring $R$, if the product of their leading coefficients is nonzero (i.e., $\text{lc}(p) \cdot \text{lc}(q) \neq 0$), then the degree of their product is the sum of their degrees: $$\deg(p \cdot q) = \deg(p) + \deg(q).$$
Polynomial.Monic.degree_mul theorem
(hq : Monic q) : degree (p * q) = degree p + degree q
Full source 
theorem Monic.degree_mul (hq : Monic q) : degree (p * q) = degree p + degree q :=
  letI := Classical.decEq R
  if hp : p = 0 then by simp [hp]
  else degree_mul' <| by rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]
Degree of Product with Monic Polynomial: $\deg(p \cdot q) = \deg(p) + \deg(q)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and a monic polynomial $q$ (i.e., a polynomial with leading coefficient $1$), the degree of the product $p \cdot q$ is equal to the sum of the degrees of $p$ and $q$: $$\deg(p \cdot q) = \deg(p) + \deg(q).$$
Polynomial.natDegree_mul' theorem
(h : leadingCoeff p * leadingCoeff q ≠ 0) : natDegree (p * q) = natDegree p + natDegree q
Full source 
theorem natDegree_mul' (h : leadingCoeffleadingCoeff p * leadingCoeff q ≠ 0) :
    natDegree (p * q) = natDegree p + natDegree q :=
  have hp : p ≠ 0 := mt leadingCoeff_eq_zero.2 fun h₁ => h <| by rw [h₁, zero_mul]
  have hq : q ≠ 0 := mt leadingCoeff_eq_zero.2 fun h₁ => h <| by rw [h₁, mul_zero]
  natDegree_eq_of_degree_eq_some <| by
    rw [degree_mul' h, Nat.cast_add, degree_eq_natDegree hp, degree_eq_natDegree hq]
Natural Degree of Polynomial Product: $\text{natDegree}(p \cdot q) = \text{natDegree}(p) + \text{natDegree}(q)$ when $\text{lc}(p)\text{lc}(q) \neq 0$
Informal description
For any two univariate polynomials $p$ and $q$ over a semiring $R$, if the product of their leading coefficients is nonzero (i.e., $\text{lc}(p) \cdot \text{lc}(q) \neq 0$), then the natural degree of their product is the sum of their natural degrees: $$\text{natDegree}(p \cdot q) = \text{natDegree}(p) + \text{natDegree}(q).$$
Polynomial.leadingCoeff_mul' theorem
(h : leadingCoeff p * leadingCoeff q ≠ 0) : leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
Full source 
theorem leadingCoeff_mul' (h : leadingCoeffleadingCoeff p * leadingCoeff q ≠ 0) :
    leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q := by
  unfold leadingCoeff
  rw [natDegree_mul' h, coeff_mul_degree_add_degree]
  rfl
Leading Coefficient of Polynomial Product: $\text{lc}(p \cdot q) = \text{lc}(p) \cdot \text{lc}(q)$ when $\text{lc}(p)\text{lc}(q) \neq 0$
Informal description
For any two univariate polynomials $p$ and $q$ over a semiring $R$, if the product of their leading coefficients is nonzero (i.e., $\text{lc}(p) \cdot \text{lc}(q) \neq 0$), then the leading coefficient of their product $p \cdot q$ is equal to the product of their leading coefficients: $$\text{lc}(p \cdot q) = \text{lc}(p) \cdot \text{lc}(q).$$
Polynomial.leadingCoeff_pow' theorem
: leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
Full source 
theorem leadingCoeff_pow' : leadingCoeffleadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n :=
  Nat.recOn n (by simp) fun n ih h => by
    have h₁ : leadingCoeffleadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeffleadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ', ← ih h₁] at h
    rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]
Leading Coefficient of Polynomial Power: $\text{lc}(p^n) = \text{lc}(p)^n$ when $\text{lc}(p)^n \neq 0$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, if the $n$-th power of the leading coefficient of $p$ is nonzero (i.e., $(\text{lc}(p))^n \neq 0$), then the leading coefficient of $p^n$ is equal to the $n$-th power of the leading coefficient of $p$: $$\text{lc}(p^n) = (\text{lc}(p))^n.$$
Polynomial.degree_pow' theorem
: ∀ {n : ℕ}, leadingCoeff p ^ n ≠ 0 → degree (p ^ n) = n • degree p
Full source 
theorem degree_pow' : ∀ {n : ℕ}, leadingCoeffleadingCoeff p ^ n ≠ 0 → degree (p ^ n) = n • degree p
  | 0 => fun h => by rw [pow_zero, ← C_1] at *; rw [degree_C h, zero_nsmul]
  | n + 1 => fun h => by
    have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0 := by
      rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
    rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]
Degree of Polynomial Power: $\deg(p^n) = n \cdot \deg(p)$ when $\text{lc}(p)^n \neq 0$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, if the $n$-th power of the leading coefficient of $p$ is nonzero (i.e., $(\text{lc}(p))^n \neq 0$), then the degree of $p^n$ is equal to $n$ times the degree of $p$: $$\deg(p^n) = n \cdot \deg(p).$$
Polynomial.natDegree_pow' theorem
{n : ℕ} (h : leadingCoeff p ^ n ≠ 0) : natDegree (p ^ n) = n * natDegree p
Full source 
theorem natDegree_pow' {n : ℕ} (h : leadingCoeffleadingCoeff p ^ n ≠ 0) : natDegree (p ^ n) = n * natDegree p :=
  letI := Classical.decEq R
  if hp0 : p = 0 then
    if hn0 : n = 0 then by simp [*] else by rw [hp0, zero_pow hn0]; simp
  else
    have hpn : p ^ n ≠ 0 := fun hpn0 => by
      have h1 := h
      rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h; exact h rfl
    Option.some_inj.1 <|
      show (natDegree (p ^ n) : WithBot ℕ) = (n * natDegree p : ℕ) by
        rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0]; simp
Natural Degree of Polynomial Power: $\text{natDegree}(p^n) = n \cdot \text{natDegree}(p)$ when $\text{lc}(p)^n \neq 0$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, if the $n$-th power of the leading coefficient of $p$ is nonzero (i.e., $(\text{lc}(p))^n \neq 0$), then the degree of $p^n$ as a natural number is equal to $n$ times the degree of $p$: $$\text{natDegree}(p^n) = n \cdot \text{natDegree}(p).$$
Polynomial.leadingCoeff_monic_mul theorem
{p q : R[X]} (hp : Monic p) : leadingCoeff (p * q) = leadingCoeff q
Full source 
theorem leadingCoeff_monic_mul {p q : R[X]} (hp : Monic p) :
    leadingCoeff (p * q) = leadingCoeff q := by
  rcases eq_or_ne q 0 with (rfl | H)
  · simp
  · rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]
    rwa [hp.leadingCoeff, one_mul, Ne, leadingCoeff_eq_zero]
Leading coefficient of product with monic polynomial: $\text{lc}(p \cdot q) = \text{lc}(q)$ when $p$ is monic
Informal description
For any univariate polynomials $p$ and $q$ over a semiring $R$, if $p$ is monic (i.e., its leading coefficient is $1$), then the leading coefficient of the product $p \cdot q$ equals the leading coefficient of $q$, i.e., $\text{lc}(p \cdot q) = \text{lc}(q)$.
Polynomial.leadingCoeff_mul_monic theorem
{p q : R[X]} (hq : Monic q) : leadingCoeff (p * q) = leadingCoeff p
Full source 
theorem leadingCoeff_mul_monic {p q : R[X]} (hq : Monic q) :
    leadingCoeff (p * q) = leadingCoeff p :=
  letI := Classical.decEq R
  Decidable.byCases
    (fun H : leadingCoeff p = 0 => by
      rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero])
    fun H : leadingCoeffleadingCoeff p ≠ 0 => by
      rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]
      rwa [hq.leadingCoeff, mul_one]
Leading Coefficient of Product with Monic Polynomial: $\text{lc}(p \cdot q) = \text{lc}(p)$ when $q$ is monic
Informal description
For any univariate polynomials $p$ and $q$ over a semiring $R$, if $q$ is monic (i.e., its leading coefficient is 1), then the leading coefficient of the product $p \cdot q$ equals the leading coefficient of $p$: $$\text{lc}(p \cdot q) = \text{lc}(p).$$
Polynomial.degree_C_mul_of_isUnit theorem
(ha : IsUnit a) (p : R[X]) : (C a * p).degree = p.degree
Full source 
lemma degree_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) : (C a * p).degree = p.degree := by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  nontriviality R
  rw [degree_mul', degree_C ha.ne_zero]
  · simp
  · simpa [ha.mul_right_eq_zero]
Degree Preservation under Multiplication by Unit Constant: $\deg(C(a) \cdot p) = \deg(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any unit $a \in R$, the degree of the product of the constant polynomial $C(a)$ and $p$ is equal to the degree of $p$, i.e., $\deg(C(a) \cdot p) = \deg(p)$.
Polynomial.degree_mul_C_of_isUnit theorem
(ha : IsUnit a) (p : R[X]) : (p * C a).degree = p.degree
Full source 
lemma degree_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) : (p * C a).degree = p.degree := by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  nontriviality R
  rw [degree_mul', degree_C ha.ne_zero]
  · simp
  · simpa [ha.mul_left_eq_zero]
Degree Preservation under Multiplication by a Unit Polynomial: $\deg(p \cdot C(a)) = \deg(p)$ for $a$ a unit
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any unit $a \in R$, the degree of the product $p \cdot C(a)$ is equal to the degree of $p$, i.e., $\deg(p \cdot C(a)) = \deg(p)$.
Polynomial.natDegree_C_mul_of_isUnit theorem
(ha : IsUnit a) (p : R[X]) : (C a * p).natDegree = p.natDegree
Full source 
lemma natDegree_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) : (C a * p).natDegree = p.natDegree := by
  simp [natDegree, degree_C_mul_of_isUnit ha]
Degree Preservation under Multiplication by Unit Constant: $\deg(C(a) \cdot p) = \deg(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any unit $a \in R$, the degree of the product of the constant polynomial $C(a)$ and $p$ is equal to the degree of $p$, i.e., $\deg(C(a) \cdot p) = \deg(p)$.
Polynomial.natDegree_mul_C_of_isUnit theorem
(ha : IsUnit a) (p : R[X]) : (p * C a).natDegree = p.natDegree
Full source 
lemma natDegree_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) : (p * C a).natDegree = p.natDegree := by
  simp [natDegree, degree_mul_C_of_isUnit ha]
Degree Preservation under Multiplication by a Unit Polynomial: $\deg(p \cdot C(a)) = \deg(p)$ for $a$ a unit
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any unit $a \in R$, the degree (as a natural number) of the product $p \cdot C(a)$ is equal to the degree of $p$, i.e., $\deg(p \cdot C(a)) = \deg(p)$.
Polynomial.leadingCoeff_C_mul_of_isUnit theorem
(ha : IsUnit a) (p : R[X]) : (C a * p).leadingCoeff = a * p.leadingCoeff
Full source 
lemma leadingCoeff_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) :
    (C a * p).leadingCoeff = a * p.leadingCoeff := by
  rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]
Leading Coefficient of Unit-Scaled Polynomial: $\text{lc}(C(a) \cdot p) = a \cdot \text{lc}(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any unit $a \in R$, the leading coefficient of the product $C(a) \cdot p$ is equal to $a$ multiplied by the leading coefficient of $p$, i.e., $$\text{lc}(C(a) \cdot p) = a \cdot \text{lc}(p).$$
Polynomial.leadingCoeff_mul_C_of_isUnit theorem
(ha : IsUnit a) (p : R[X]) : (p * C a).leadingCoeff = p.leadingCoeff * a
Full source 
lemma leadingCoeff_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) :
    (p * C a).leadingCoeff = p.leadingCoeff * a := by
  rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]
Leading Coefficient of Polynomial Multiplied by Unit: $\text{lc}(p \cdot C(a)) = \text{lc}(p) \cdot a$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any unit $a \in R$, the leading coefficient of the product $p \cdot C(a)$ is equal to the product of the leading coefficient of $p$ and $a$, i.e., $$\text{lc}(p \cdot C(a)) = \text{lc}(p) \cdot a.$$
Polynomial.leadingCoeff_mul_X_pow theorem
{p : R[X]} {n : ℕ} : leadingCoeff (p * X ^ n) = leadingCoeff p
Full source 
@[simp]
theorem leadingCoeff_mul_X_pow {p : R[X]} {n : ℕ} : leadingCoeff (p * X ^ n) = leadingCoeff p :=
  leadingCoeff_mul_monic (monic_X_pow n)
Leading Coefficient of Product with $X^n$: $\text{lc}(p \cdot X^n) = \text{lc}(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, the leading coefficient of the product $p \cdot X^n$ equals the leading coefficient of $p$, i.e., $$\text{lc}(p \cdot X^n) = \text{lc}(p).$$
Polynomial.leadingCoeff_mul_X theorem
{p : R[X]} : leadingCoeff (p * X) = leadingCoeff p
Full source 
@[simp]
theorem leadingCoeff_mul_X {p : R[X]} : leadingCoeff (p * X) = leadingCoeff p :=
  leadingCoeff_mul_monic monic_X
Leading Coefficient of Polynomial Multiplied by $X$: $\text{lc}(p \cdot X) = \text{lc}(p)$
Informal description
For any univariate polynomial $p$ over a semiring $R$, the leading coefficient of the product $p \cdot X$ is equal to the leading coefficient of $p$, i.e., $$\text{lc}(p \cdot X) = \text{lc}(p).$$
Polynomial.coeff_pow_mul_natDegree theorem
(p : R[X]) (n : ℕ) : (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n
Full source 
@[simp]
theorem coeff_pow_mul_natDegree (p : R[X]) (n : ℕ) :
    (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n := by
  induction n with
  | zero => simp
  | succ i hi =>
    rw [pow_succ, pow_succ, Nat.succ_mul]
    by_cases hp1 : p.leadingCoeff ^ i = 0
    · rw [hp1, zero_mul]
      by_cases hp2 : p ^ i = 0
      · rw [hp2, zero_mul, coeff_zero]
      · apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := add_lt_add_right h1 _

    · rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
      exact coeff_mul_degree_add_degree _ _
Coefficient of Highest Degree Term in Polynomial Power: $(p^n)_{n \cdot \deg(p)} = \text{lc}(p)^n$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, the coefficient of $X^{n \cdot \deg(p)}$ in $p^n$ equals the $n$-th power of the leading coefficient of $p$, i.e., $$(p^n)_{n \cdot \deg(p)} = (\text{lc}(p))^n.$$
Polynomial.coeff_mul_add_eq_of_natDegree_le theorem
{df dg : ℕ} {f g : R[X]} (hdf : natDegree f ≤ df) (hdg : natDegree g ≤ dg) : (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
Full source 
theorem coeff_mul_add_eq_of_natDegree_le {df dg : ℕ} {f g : R[X]}
    (hdf : natDegree f ≤ df) (hdg : natDegree g ≤ dg) :
    (f * g).coeff (df + dg) = f.coeff df * g.coeff dg := by
  rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]
  · rw [mem_antidiagonal]
  rintro ⟨df', dg'⟩ hmem hne
  obtain h | hdf' := lt_or_le df df'
  · rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]
  obtain h | hdg' := lt_or_le dg dg'
  · rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]
  obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
  exact (hne rfl).elim
Coefficient of Product at Sum of Degrees: $(f \cdot g)_{df + dg} = f_{df} \cdot g_{dg}$
Informal description
Let $R$ be a semiring and let $f, g \in R[X]$ be univariate polynomials over $R$. For any natural numbers $df$ and $dg$ such that the natural degree of $f$ is at most $df$ and the natural degree of $g$ is at most $dg$, the coefficient of $X^{df + dg}$ in the product $f \cdot g$ is equal to the product of the coefficient of $X^{df}$ in $f$ and the coefficient of $X^{dg}$ in $g$. In other words: $$(f \cdot g)_{df + dg} = f_{df} \cdot g_{dg}.$$
Polynomial.degree_smul_le theorem
(a : R) (p : R[X]) : degree (a • p) ≤ degree p
Full source 
theorem degree_smul_le (a : R) (p : R[X]) : degree (a • p) ≤ degree p := by
  refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
  rw [degree_lt_iff_coeff_zero] at hm
  simp [hm m le_rfl]
Degree Bound for Scalar Multiplication of Polynomials: $\deg(a \cdot p) \leq \deg(p)$
Informal description
For any element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the degree of the scalar multiple $a \cdot p$ is less than or equal to the degree of $p$.
Polynomial.natDegree_smul_le theorem
(a : R) (p : R[X]) : natDegree (a • p) ≤ natDegree p
Full source 
theorem natDegree_smul_le (a : R) (p : R[X]) : natDegree (a • p) ≤ natDegree p :=
  natDegree_le_natDegree (degree_smul_le a p)
Natural Degree Bound for Scalar Multiplication of Polynomials: $\text{natDegree}(a \cdot p) \leq \text{natDegree}(p)$
Informal description
For any element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the natural degree of the scalar multiple $a \cdot p$ is less than or equal to the natural degree of $p$.
Polynomial.degree_smul_of_isRightRegular_leadingCoeff theorem
(ha : a ≠ 0) (hp : IsRightRegular p.leadingCoeff) : (a • p).degree = p.degree
Full source 
theorem degree_smul_of_isRightRegular_leadingCoeff (ha : a ≠ 0)
    (hp : IsRightRegular p.leadingCoeff) : (a • p).degree = p.degree := by
  refine le_antisymm (degree_smul_le a p) <| degree_le_degree ?_
  rw [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq]
  exact hp.mul_right_eq_zero_iff.ne.mpr ha
Degree Preservation under Scalar Multiplication with Right-Regular Leading Coefficient: $\deg(a \cdot p) = \deg(p)$
Informal description
For any nonzero element $a$ in a semiring $R$ and any nonzero polynomial $p \in R[X]$ whose leading coefficient is right-regular (i.e., right multiplication by the leading coefficient is injective), the degree of the scalar multiple $a \cdot p$ is equal to the degree of $p$, i.e., $$\deg(a \cdot p) = \deg(p).$$
Polynomial.degree_lt_degree_mul_X theorem
(hp : p ≠ 0) : p.degree < (p * X).degree
Full source 
theorem degree_lt_degree_mul_X (hp : p ≠ 0) : p.degree < (p * X).degree := by
  haveI := Nontrivial.of_polynomial_ne hp
  have : leadingCoeffleadingCoeff p * leadingCoeff X ≠ 0 := by simpa
  rw [degree_mul' this, degree_eq_natDegree hp, degree_X, ← Nat.cast_one, ← Nat.cast_add]
  norm_cast
  exact Nat.lt_succ_self _
Degree Inequality: $\deg(p) < \deg(p \cdot X)$ for $p \neq 0$
Informal description
For any nonzero polynomial $p$ in $R[X]$, the degree of $p$ is strictly less than the degree of the product $p \cdot X$, i.e., $\deg(p) < \deg(p \cdot X)$.
Polynomial.degree_sum_fin_lt theorem
{n : ℕ} (f : Fin n → R) : degree (∑ i : Fin n, C (f i) * X ^ (i : ℕ)) < n
Full source 
theorem degree_sum_fin_lt {n : ℕ} (f : Fin n → R) :
    degree (∑ i : Fin n, C (f i) * X ^ (i : ℕ)) < n :=
  (degree_sum_le _ _).trans_lt <|
    (Finset.sup_lt_iff <| WithBot.bot_lt_coe n).2 fun k _hk =>
      (degree_C_mul_X_pow_le _ _).trans_lt <| WithBot.coe_lt_coe.2 k.is_lt
Degree Bound for Finite Sum of Monomials: $\deg(\sum_{i < n} f(i) X^i) < n$
Informal description
For any natural number $n$ and any function $f \colon \mathrm{Fin}(n) \to R$, the degree of the polynomial $\sum_{i \in \mathrm{Fin}(n)} f(i) X^i$ is strictly less than $n$.
Polynomial.degree_C_lt_degree_C_mul_X theorem
(ha : a ≠ 0) : degree (C b) < degree (C a * X)
Full source 
theorem degree_C_lt_degree_C_mul_X (ha : a ≠ 0) : degree (C b) < degree (C a * X) := by
  simpa only [degree_C_mul_X ha] using degree_C_lt
Degree Inequality: $\deg(C(b)) < \deg(C(a)X)$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a semiring $R$, the degree of the constant polynomial $C(b)$ is strictly less than the degree of the polynomial $C(a) \cdot X$.
Polynomial.natDegree_mul_X theorem
(hp : p ≠ 0) : natDegree (p * X) = natDegree p + 1
Full source 
@[simp] lemma natDegree_mul_X (hp : p ≠ 0) : natDegree (p * X) = natDegree p + 1 := by
  rw [natDegree_mul' (by simpa), natDegree_X]
Natural Degree of Polynomial Multiplied by $X$: $\text{natDegree}(p \cdot X) = \text{natDegree}(p) + 1$ for $p \neq 0$
Informal description
For any nonzero polynomial $p$ over a semiring $R$, the natural degree of the product $p \cdot X$ is equal to the natural degree of $p$ plus one, i.e., $\text{natDegree}(p \cdot X) = \text{natDegree}(p) + 1$.
Polynomial.natDegree_X_mul theorem
(hp : p ≠ 0) : natDegree (X * p) = natDegree p + 1
Full source 
@[simp] lemma natDegree_X_mul (hp : p ≠ 0) : natDegree (X * p) = natDegree p + 1 := by
  rw [commute_X p, natDegree_mul_X hp]
Natural Degree of $X \cdot p$: $\text{natDegree}(X \cdot p) = \text{natDegree}(p) + 1$ for $p \neq 0$
Informal description
For any nonzero polynomial $p$ over a semiring $R$, the natural degree of the product $X \cdot p$ is equal to the natural degree of $p$ plus one, i.e., $\text{natDegree}(X \cdot p) = \text{natDegree}(p) + 1$.
Polynomial.natDegree_mul_X_pow theorem
(hp : p ≠ 0) : natDegree (p * X ^ n) = natDegree p + n
Full source 
@[simp] lemma natDegree_mul_X_pow (hp : p ≠ 0) : natDegree (p * X ^ n) = natDegree p + n := by
  rw [natDegree_mul' (by simpa), natDegree_X_pow]
Natural Degree of Polynomial Multiplied by $X^n$: $\text{natDegree}(p \cdot X^n) = \text{natDegree}(p) + n$ for $p \neq 0$
Informal description
For any nonzero polynomial $p$ over a semiring $R$ and any natural number $n$, the natural degree of the product $p \cdot X^n$ is equal to the sum of the natural degree of $p$ and $n$, i.e., $$\text{natDegree}(p \cdot X^n) = \text{natDegree}(p) + n.$$
Polynomial.natDegree_X_pow_mul theorem
(hp : p ≠ 0) : natDegree (X ^ n * p) = natDegree p + n
Full source 
@[simp] lemma natDegree_X_pow_mul (hp : p ≠ 0) : natDegree (X ^ n * p) = natDegree p + n := by
  rw [commute_X_pow, natDegree_mul_X_pow n hp]
Natural Degree of $X^n \cdot p$: $\text{natDegree}(X^n \cdot p) = \text{natDegree}(p) + n$ for $p \neq 0$
Informal description
For any nonzero polynomial $p$ over a semiring $R$ and any natural number $n$, the natural degree of the product $X^n \cdot p$ is equal to the sum of the natural degree of $p$ and $n$, i.e., $$\text{natDegree}(X^n \cdot p) = \text{natDegree}(p) + n.$$
Polynomial.natDegree_X_pow_le theorem
{R : Type*} [Semiring R] (n : ℕ) : (X ^ n : R[X]).natDegree ≤ n
Full source 
theorem natDegree_X_pow_le {R : Type*} [Semiring R] (n : ℕ) : (X ^ n : R[X]).natDegree ≤ n := by
  nontriviality R
  rw [Polynomial.natDegree_X_pow]
Upper Bound on Degree of $X^n$: $\text{natDegree}(X^n) \leq n$
Informal description
For any natural number $n$ and any semiring $R$, the natural degree of the polynomial $X^n$ in $R[X]$ is less than or equal to $n$, i.e., $$\text{natDegree}(X^n) \leq n.$$
Polynomial.not_isUnit_X theorem
: ¬IsUnit (X : R[X])
Full source 
theorem not_isUnit_X : ¬IsUnit (X : R[X]) := fun ⟨⟨_, g, _hfg, hgf⟩, rfl⟩ =>
  zero_ne_one' R <| by
    rw [← coeff_one_zero, ← hgf]
    simp
Non-unit Property of the Polynomial Variable $X$
Informal description
The polynomial variable $X$ in the polynomial ring $R[X]$ is not a unit, i.e., there does not exist a polynomial $p \in R[X]$ such that $X \cdot p = 1$.
Polynomial.degree_mul_X theorem
: degree (p * X) = degree p + 1
Full source 
@[simp]
theorem degree_mul_X : degree (p * X) = degree p + 1 := by simp [monic_X.degree_mul]
Degree of Polynomial Multiplied by $X$: $\deg(p \cdot X) = \deg(p) + 1$
Informal description
For any univariate polynomial $p$ over a semiring $R$, the degree of the product $p \cdot X$ is equal to the degree of $p$ plus one, i.e., $$\deg(p \cdot X) = \deg(p) + 1.$$
Polynomial.degree_mul_X_pow theorem
: degree (p * X ^ n) = degree p + n
Full source 
@[simp]
theorem degree_mul_X_pow : degree (p * X ^ n) = degree p + n := by simp [(monic_X_pow n).degree_mul]
Degree of Product with Monomial: $\deg(p \cdot X^n) = \deg(p) + n$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, the degree of the product $p \cdot X^n$ is equal to the degree of $p$ plus $n$, i.e., $$\deg(p \cdot X^n) = \deg(p) + n.$$
Polynomial.degree_sub_C theorem
(hp : 0 < degree p) : degree (p - C a) = degree p
Full source 
theorem degree_sub_C (hp : 0 < degree p) : degree (p - C a) = degree p := by
  rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]
Degree Preservation Under Constant Subtraction: $\deg(p - C(a)) = \deg(p)$ for $\deg(p) > 0$
Informal description
For any univariate polynomial $p$ over a ring $R$ with positive degree and any constant $a \in R$, the degree of the difference $p - C(a)$ equals the degree of $p$, i.e., $\deg(p - C(a)) = \deg(p)$.
Polynomial.natDegree_sub_C theorem
{a : R} : natDegree (p - C a) = natDegree p
Full source 
@[simp]
theorem natDegree_sub_C {a : R} : natDegree (p - C a) = natDegree p := by
  rw [sub_eq_add_neg, ← C_neg, natDegree_add_C]
Natural Degree Invariance Under Constant Subtraction: $\text{natDegree}(p - C(a)) = \text{natDegree}(p)$
Informal description
For any univariate polynomial $p$ over a ring $R$ and any constant $a \in R$, the natural degree of the difference $p - C(a)$ equals the natural degree of $p$, i.e., $$\text{natDegree}(p - C(a)) = \text{natDegree}(p).$$
Polynomial.leadingCoeff_sub_of_degree_lt theorem
(h : Polynomial.degree q < Polynomial.degree p) : (p - q).leadingCoeff = p.leadingCoeff
Full source 
theorem leadingCoeff_sub_of_degree_lt (h : Polynomial.degree q < Polynomial.degree p) :
    (p - q).leadingCoeff = p.leadingCoeff := by
  rw [← q.degree_neg] at h
  rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt' h]
Leading Coefficient of Difference When Second Polynomial Has Lower Degree: $\text{lc}(p - q) = \text{lc}(p)$ if $\deg(q) < \deg(p)$
Informal description
For univariate polynomials $p$ and $q$ over a ring $R$, if the degree of $q$ is strictly less than the degree of $p$, then the leading coefficient of their difference $p - q$ equals the leading coefficient of $p$, i.e., $$\text{lc}(p - q) = \text{lc}(p).$$
Polynomial.leadingCoeff_sub_of_degree_lt' theorem
(h : Polynomial.degree p < Polynomial.degree q) : (p - q).leadingCoeff = -q.leadingCoeff
Full source 
theorem leadingCoeff_sub_of_degree_lt' (h : Polynomial.degree p < Polynomial.degree q) :
    (p - q).leadingCoeff = -q.leadingCoeff := by
  rw [← q.degree_neg] at h
  rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]
Leading Coefficient of Difference When First Polynomial Has Lower Degree: $\text{lc}(p - q) = -\text{lc}(q)$ if $\deg(p) < \deg(q)$
Informal description
For univariate polynomials $p$ and $q$ over a ring $R$, if the degree of $p$ is strictly less than the degree of $q$, then the leading coefficient of their difference $p - q$ is equal to the negation of the leading coefficient of $q$, i.e., $$\text{lc}(p - q) = -\text{lc}(q).$$
Polynomial.leadingCoeff_sub_of_degree_eq theorem
(h : degree p = degree q) (hlc : leadingCoeff p ≠ leadingCoeff q) : leadingCoeff (p - q) = leadingCoeff p - leadingCoeff q
Full source 
theorem leadingCoeff_sub_of_degree_eq (h : degree p = degree q)
    (hlc : leadingCoeffleadingCoeff p ≠ leadingCoeff q) :
    leadingCoeff (p - q) = leadingCoeff p - leadingCoeff q := by
  replace h : degree p = degree (-q) := by rwa [q.degree_neg]
  replace hlc : leadingCoeffleadingCoeff p + leadingCoeff (-q) ≠ 0 := by
    rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
  rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]
Leading Coefficient of Difference When Degrees Are Equal and Leading Coefficients Are Distinct: $\text{lc}(p - q) = \text{lc}(p) - \text{lc}(q)$
Informal description
For univariate polynomials $p$ and $q$ over a ring $R$, if $p$ and $q$ have the same degree and their leading coefficients are distinct, then the leading coefficient of their difference $p - q$ equals the difference of their leading coefficients, i.e., $$\text{lc}(p - q) = \text{lc}(p) - \text{lc}(q).$$
Polynomial.degree_sub_eq_left_of_degree_lt theorem
(h : degree q < degree p) : degree (p - q) = degree p
Full source 
theorem degree_sub_eq_left_of_degree_lt (h : degree q < degree p) : degree (p - q) = degree p := by
  rw [← degree_neg q] at h
  rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]
Degree of Difference When Second Term Has Lower Degree: $\deg(p - q) = \deg(p)$ if $\deg(q) < \deg(p)$
Informal description
For any univariate polynomials $p$ and $q$ over a ring, if the degree of $q$ is strictly less than the degree of $p$, then the degree of the difference $p - q$ is equal to the degree of $p$, i.e., $\deg(p - q) = \deg(p)$.
Polynomial.degree_sub_eq_right_of_degree_lt theorem
(h : degree p < degree q) : degree (p - q) = degree q
Full source 
theorem degree_sub_eq_right_of_degree_lt (h : degree p < degree q) : degree (p - q) = degree q := by
  rw [← degree_neg q] at h
  rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]
Degree of Difference When First Term Has Lower Degree: $\deg(p - q) = \deg(q)$ if $\deg(p) < \deg(q)$
Informal description
For any univariate polynomials $p$ and $q$ over a ring, if the degree of $p$ is strictly less than the degree of $q$, then the degree of the difference $p - q$ is equal to the degree of $q$, i.e., $\deg(p - q) = \deg(q)$.
Polynomial.natDegree_sub_eq_left_of_natDegree_lt theorem
(h : natDegree q < natDegree p) : natDegree (p - q) = natDegree p
Full source 
theorem natDegree_sub_eq_left_of_natDegree_lt (h : natDegree q < natDegree p) :
    natDegree (p - q) = natDegree p :=
  natDegree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt (degree_lt_degree h))
Natural Degree of Difference When Second Term Has Lower Natural Degree: $\deg_{\mathbb{N}}(p - q) = \deg_{\mathbb{N}}(p)$ if $\deg_{\mathbb{N}}(q) < \deg_{\mathbb{N}}(p)$
Informal description
For any univariate polynomials $p$ and $q$ over a ring, if the natural degree of $q$ is strictly less than the natural degree of $p$, then the natural degree of the difference $p - q$ is equal to the natural degree of $p$, i.e., $\deg_{\mathbb{N}}(p - q) = \deg_{\mathbb{N}}(p)$.
Polynomial.natDegree_sub_eq_right_of_natDegree_lt theorem
(h : natDegree p < natDegree q) : natDegree (p - q) = natDegree q
Full source 
theorem natDegree_sub_eq_right_of_natDegree_lt (h : natDegree p < natDegree q) :
    natDegree (p - q) = natDegree q :=
  natDegree_eq_of_degree_eq (degree_sub_eq_right_of_degree_lt (degree_lt_degree h))
Natural Degree of Difference When First Term Has Lower Natural Degree: $\deg_{\mathbb{N}}(p - q) = \deg_{\mathbb{N}}(q)$ if $\deg_{\mathbb{N}}(p) < \deg_{\mathbb{N}}(q)$
Informal description
For any univariate polynomials $p$ and $q$ over a ring, if the natural degree of $p$ is strictly less than the natural degree of $q$, then the natural degree of the difference $p - q$ is equal to the natural degree of $q$, i.e., $\deg_{\mathbb{N}}(p - q) = \deg_{\mathbb{N}}(q)$.
Polynomial.degree_X_add_C theorem
(a : R) : degree (X + C a) = 1
Full source 
@[simp]
theorem degree_X_add_C (a : R) : degree (X + C a) = 1 := by
  have : degree (C a) < degree (X : R[X]) :=
    calc
      degree (C a) ≤ 0 := degree_C_le
      _ < 1 := WithBot.coe_lt_coe.mpr zero_lt_one
      _ = degree X := degree_X.symm
  rw [degree_add_eq_left_of_degree_lt this, degree_X]
Degree of Linear Polynomial: $\deg(X + a) = 1$
Informal description
For any element $a$ in a semiring $R$, the degree of the polynomial $X + a$ is equal to $1$, i.e., $\deg(X + a) = 1$.
Polynomial.natDegree_X_add_C theorem
(x : R) : (X + C x).natDegree = 1
Full source 
theorem natDegree_X_add_C (x : R) : (X + C x).natDegree = 1 :=
  natDegree_eq_of_degree_eq_some <| degree_X_add_C x
Natural Degree of Linear Polynomial: $\deg_{\mathbb{N}}(X + x) = 1$
Informal description
For any element $x$ in a semiring $R$, the natural degree of the polynomial $X + x$ is equal to $1$, i.e., $\deg_{\mathbb{N}}(X + x) = 1$.
Polynomial.nextCoeff_X_add_C theorem
[Semiring S] (c : S) : nextCoeff (X + C c) = c
Full source 
@[simp]
theorem nextCoeff_X_add_C [Semiring S] (c : S) : nextCoeff (X + C c) = c := by
  nontriviality S
  simp [nextCoeff_of_natDegree_pos]
Next Coefficient of Linear Polynomial: $\text{nextCoeff}(X + c) = c$
Informal description
For any element $c$ in a semiring $S$, the next coefficient (i.e., the coefficient of $X^0$) of the polynomial $X + c$ is equal to $c$.
Polynomial.degree_X_pow_add_C theorem
{n : ℕ} (hn : 0 < n) (a : R) : degree ((X : R[X]) ^ n + C a) = n
Full source 
theorem degree_X_pow_add_C {n : ℕ} (hn : 0 < n) (a : R) : degree ((X : R[X]) ^ n + C a) = n := by
  have : degree (C a) < degree ((X : R[X]) ^ n) := degree_C_le.trans_lt <| by
    rwa [degree_X_pow, Nat.cast_pos]
  rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]
Degree of $X^n + a$ is $n$ for $n > 0$
Informal description
For any positive natural number $n$ and any element $a$ in a semiring $R$, the degree of the polynomial $X^n + a$ is equal to $n$, i.e., $\deg(X^n + a) = n$.
Polynomial.X_pow_add_C_ne_zero theorem
{n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 0
Full source 
theorem X_pow_add_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 0 :=
  mt degree_eq_bot.2
    (show degreedegree ((X : R[X]) ^ n + C a) ≠ ⊥ by
      rw [degree_X_pow_add_C hn a]; exact WithBot.coe_ne_bot)
Non-vanishing of $X^n + a$ for $n > 0$
Informal description
For any positive natural number $n$ and any element $a$ in a semiring $R$, the polynomial $X^n + a$ is not equal to the zero polynomial, i.e., $X^n + a \neq 0$.
Polynomial.X_add_C_ne_zero theorem
(r : R) : X + C r ≠ 0
Full source 
theorem X_add_C_ne_zero (r : R) : XX + C r ≠ 0 :=
  pow_one (X : R[X]) ▸ X_pow_add_C_ne_zero zero_lt_one r
Non-vanishing of linear polynomial $X + r$
Informal description
For any element $r$ in a semiring $R$, the polynomial $X + r$ is not equal to the zero polynomial, i.e., $X + r \neq 0$.
Polynomial.zero_nmem_multiset_map_X_add_C theorem
{α : Type*} (m : Multiset α) (f : α → R) : (0 : R[X]) ∉ m.map fun a => X + C (f a)
Full source 
theorem zero_nmem_multiset_map_X_add_C {α : Type*} (m : Multiset α) (f : α → R) :
    (0 : R[X]) ∉ m.map fun a => X + C (f a) := fun mem =>
  let ⟨_a, _, ha⟩ := Multiset.mem_map.mp mem
  X_add_C_ne_zero _ ha
Non-vanishing of linear polynomials in mapped multiset
Informal description
For any multiset $m$ over a type $\alpha$ and any function $f \colon \alpha \to R$, the zero polynomial $0$ is not an element of the multiset obtained by mapping each $a \in m$ to the linear polynomial $X + f(a)$.
Polynomial.natDegree_X_pow_add_C theorem
{n : ℕ} {r : R} : (X ^ n + C r).natDegree = n
Full source 
theorem natDegree_X_pow_add_C {n : ℕ} {r : R} : (X ^ n + C r).natDegree = n := by
  by_cases hn : n = 0
  · rw [hn, pow_zero, ← C_1, ← RingHom.map_add, natDegree_C]
  · exact natDegree_eq_of_degree_eq_some (degree_X_pow_add_C (pos_iff_ne_zero.mpr hn) r)
Degree of $X^n + r$ is $n$
Informal description
For any natural number $n$ and any element $r$ in a semiring $R$, the degree of the polynomial $X^n + r$ is equal to $n$, i.e., $\deg(X^n + r) = n$.
Polynomial.X_pow_add_C_ne_one theorem
{n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 1
Full source 
theorem X_pow_add_C_ne_one {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 1 := fun h =>
  hn.ne' <| by simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h
Non-identity of $X^n + a$ for $n > 0$
Informal description
For any natural number $n > 0$ and any element $a$ in a semiring $R$, the polynomial $X^n + a$ is not equal to the constant polynomial $1$.
Polynomial.X_add_C_ne_one theorem
(r : R) : X + C r ≠ 1
Full source 
theorem X_add_C_ne_one (r : R) : XX + C r ≠ 1 :=
  pow_one (X : R[X]) ▸ X_pow_add_C_ne_one zero_lt_one r
Non-identity of $X + r$ in Polynomial Ring $R[X]$
Informal description
For any element $r$ in a semiring $R$, the polynomial $X + r$ is not equal to the constant polynomial $1$, i.e., $X + r \neq 1$.
Polynomial.leadingCoeff_X_pow_add_C theorem
{n : ℕ} (hn : 0 < n) {r : R} : (X ^ n + C r).leadingCoeff = 1
Full source 
@[simp]
theorem leadingCoeff_X_pow_add_C {n : ℕ} (hn : 0 < n) {r : R} :
    (X ^ n + C r).leadingCoeff = 1 := by
  nontriviality R
  rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
Leading coefficient of $X^n + r$ is $1$ for $n > 0$
Informal description
For any natural number $n > 0$ and any element $r$ in a semiring $R$, the leading coefficient of the polynomial $X^n + r$ is equal to $1$.
Polynomial.leadingCoeff_X_pow_add_one theorem
{n : ℕ} (hn : 0 < n) : (X ^ n + 1 : R[X]).leadingCoeff = 1
Full source 
@[simp]
theorem leadingCoeff_X_pow_add_one {n : ℕ} (hn : 0 < n) : (X ^ n + 1 : R[X]).leadingCoeff = 1 :=
  leadingCoeff_X_pow_add_C hn
Leading coefficient of $X^n + 1$ is $1$ for $n > 0$
Informal description
For any natural number $n > 0$, the leading coefficient of the polynomial $X^n + 1$ in the polynomial ring $R[X]$ is equal to $1$.
Polynomial.leadingCoeff_pow_X_add_C theorem
(r : R) (i : ℕ) : leadingCoeff ((X + C r) ^ i) = 1
Full source 
@[simp]
theorem leadingCoeff_pow_X_add_C (r : R) (i : ℕ) : leadingCoeff ((X + C r) ^ i) = 1 := by
  nontriviality
  rw [leadingCoeff_pow'] <;> simp
Leading coefficient of $(X + r)^i$ is $1$
Informal description
For any element $r$ in a semiring $R$ and any natural number $i$, the leading coefficient of the polynomial $(X + r)^i$ is equal to $1$.
Polynomial.degree_mul theorem
: degree (p * q) = degree p + degree q
Full source 
@[simp]
lemma degree_mul : degree (p * q) = degree p + degree q :=
  letI := Classical.decEq R
  if hp0 : p = 0 then by simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]
  else
    if hq0 : q = 0 then by simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]
    else degree_mul' <| mul_ne_zero (mt leadingCoeff_eq_zero.1 hp0) (mt leadingCoeff_eq_zero.1 hq0)
Degree of Polynomial Product: $\deg(p \cdot q) = \deg(p) + \deg(q)$
Informal description
For any two univariate polynomials $p$ and $q$ over a semiring $R$, the degree of their product is the sum of their degrees: $$\deg(p \cdot q) = \deg(p) + \deg(q).$$
Polynomial.degreeMonoidHom definition
[Nontrivial R] : R[X] →* Multiplicative (WithBot ℕ)
Full source 
/-- `degree` as a monoid homomorphism between `R[X]` and `Multiplicative (WithBot ℕ)`.
  This is useful to prove results about multiplication and degree. -/
def degreeMonoidHom [Nontrivial R] : R[X]R[X] →* Multiplicative (WithBot ℕ) where
  toFun := degree
  map_one' := degree_one
  map_mul' _ _ := degree_mul
Degree as a monoid homomorphism for polynomials
Informal description
For a nontrivial semiring $R$, the degree function $\deg \colon R[X] \to \mathbb{N} \cup \{\bot\}$ (where $\bot$ represents the degree of the zero polynomial) is a monoid homomorphism from the multiplicative monoid of polynomials to the multiplicative monoid of $\mathbb{N} \cup \{\bot\}$. Specifically: - $\deg(1) = 0$ (where $1$ is the constant polynomial $1$), - $\deg(p \cdot q) = \deg(p) + \deg(q)$ for any polynomials $p, q \in R[X]$.
Polynomial.degree_pow theorem
[Nontrivial R] (p : R[X]) (n : ℕ) : degree (p ^ n) = n • degree p
Full source 
@[simp]
lemma degree_pow [Nontrivial R] (p : R[X]) (n : ℕ) : degree (p ^ n) = n • degree p :=
  map_pow (@degreeMonoidHom R _ _ _) _ _
Degree of Polynomial Power: $\deg(p^n) = n \cdot \deg(p)$
Informal description
For any univariate polynomial $p$ over a nontrivial semiring $R$ and any natural number $n$, the degree of $p^n$ is equal to $n$ times the degree of $p$, i.e., $$\deg(p^n) = n \cdot \deg(p).$$
Polynomial.leadingCoeff_mul theorem
(p q : R[X]) : leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
Full source 
@[simp]
lemma leadingCoeff_mul (p q : R[X]) : leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q := by
  by_cases hp : p = 0
  · simp only [hp, zero_mul, leadingCoeff_zero]
  · by_cases hq : q = 0
    · simp only [hq, mul_zero, leadingCoeff_zero]
    · rw [leadingCoeff_mul']
      exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)
Leading Coefficient of Polynomial Product: $\text{lc}(p \cdot q) = \text{lc}(p) \cdot \text{lc}(q)$
Informal description
For any two univariate polynomials $p$ and $q$ over a semiring $R$, the leading coefficient of their product $p \cdot q$ is equal to the product of their leading coefficients, i.e., $$\text{lc}(p \cdot q) = \text{lc}(p) \cdot \text{lc}(q).$$
Polynomial.leadingCoeffHom definition
: R[X] →* R
Full source 
/-- `Polynomial.leadingCoeff` bundled as a `MonoidHom` when `R` has `NoZeroDivisors`, and thus
  `leadingCoeff` is multiplicative -/
def leadingCoeffHom : R[X]R[X] →* R where
  toFun := leadingCoeff
  map_one' := by simp
  map_mul' := leadingCoeff_mul
Leading coefficient monoid homomorphism
Informal description
The monoid homomorphism that maps a univariate polynomial $p \in R[X]$ to its leading coefficient $\text{lc}(p) \in R$, where $R$ is a semiring with no zero divisors. This homomorphism preserves the multiplicative identity and the multiplication operation, i.e., $\text{lc}(1) = 1$ and $\text{lc}(p \cdot q) = \text{lc}(p) \cdot \text{lc}(q)$ for any polynomials $p, q \in R[X]$.
Polynomial.leadingCoeffHom_apply theorem
(p : R[X]) : leadingCoeffHom p = leadingCoeff p
Full source 
@[simp]
lemma leadingCoeffHom_apply (p : R[X]) : leadingCoeffHom p = leadingCoeff p :=
  rfl
Leading Coefficient Homomorphism Evaluation: $\text{leadingCoeffHom}(p) = \text{lc}(p)$
Informal description
For any univariate polynomial $p \in R[X]$, the leading coefficient homomorphism evaluated at $p$ is equal to the leading coefficient of $p$, i.e., $$\text{leadingCoeffHom}(p) = \text{lc}(p).$$
Polynomial.leadingCoeff_pow theorem
(p : R[X]) (n : ℕ) : leadingCoeff (p ^ n) = leadingCoeff p ^ n
Full source 
@[simp]
lemma leadingCoeff_pow (p : R[X]) (n : ℕ) : leadingCoeff (p ^ n) = leadingCoeff p ^ n :=
  (leadingCoeffHom : R[X]R[X] →* R).map_pow p n
Leading Coefficient of Polynomial Power: $\text{lc}(p^n) = \text{lc}(p)^n$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, the leading coefficient of $p^n$ is equal to the $n$-th power of the leading coefficient of $p$, i.e., $$\text{lc}(p^n) = (\text{lc}(p))^n.$$
Polynomial.leadingCoeff_dvd_leadingCoeff theorem
{a p : R[X]} (hap : a ∣ p) : a.leadingCoeff ∣ p.leadingCoeff
Full source 
lemma leadingCoeff_dvd_leadingCoeff {a p : R[X]} (hap : a ∣ p) :
    a.leadingCoeff ∣ p.leadingCoeff :=
  map_dvd leadingCoeffHom hap
Divisibility of Leading Coefficients in Polynomial Division
Informal description
For any univariate polynomials $a$ and $p$ over a semiring $R$ with no zero divisors, if $a$ divides $p$, then the leading coefficient of $a$ divides the leading coefficient of $p$.
Polynomial.degree_le_mul_left theorem
(p : R[X]) (hq : q ≠ 0) : degree p ≤ degree (p * q)
Full source 
lemma degree_le_mul_left (p : R[X]) (hq : q ≠ 0) : degree p ≤ degree (p * q) := by
  classical
  obtain rfl | hp := eq_or_ne p 0
  · simp
  · rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
    exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)
Degree Inequality for Polynomial Multiplication: $\deg(p) \leq \deg(p \cdot q)$
Informal description
For any univariate polynomial $p$ over a semiring $R$ and any nonzero polynomial $q$, the degree of $p$ is less than or equal to the degree of the product $p \cdot q$, i.e., $$\deg(p) \leq \deg(p \cdot q).$$
Polynomial.leadingCoeff_X_pow_sub_C theorem
{n : ℕ} (hn : 0 < n) {r : R} : (X ^ n - C r).leadingCoeff = 1
Full source 
@[simp]
theorem leadingCoeff_X_pow_sub_C {n : ℕ} (hn : 0 < n) {r : R} :
    (X ^ n - C r).leadingCoeff = 1 := by
  rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]
Leading coefficient of $X^n - r$ is $1$ for $n > 0$
Informal description
For any natural number $n > 0$ and any element $r$ in a ring $R$, the leading coefficient of the polynomial $X^n - r$ is equal to $1$.
Polynomial.leadingCoeff_X_pow_sub_one theorem
{n : ℕ} (hn : 0 < n) : (X ^ n - 1 : R[X]).leadingCoeff = 1
Full source 
@[simp]
theorem leadingCoeff_X_pow_sub_one {n : ℕ} (hn : 0 < n) : (X ^ n - 1 : R[X]).leadingCoeff = 1 :=
  leadingCoeff_X_pow_sub_C hn
Leading coefficient of $X^n - 1$ is $1$ for $n > 0$
Informal description
For any natural number $n > 0$ and any ring $R$, the leading coefficient of the polynomial $X^n - 1$ in $R[X]$ is equal to $1$.
Polynomial.degree_X_sub_C theorem
(a : R) : degree (X - C a) = 1
Full source 
@[simp]
theorem degree_X_sub_C (a : R) : degree (X - C a) = 1 := by
  rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
Degree of Linear Polynomial: $\deg(X - a) = 1$
Informal description
For any element $a$ in a ring $R$, the degree of the polynomial $X - a$ is equal to $1$, i.e., $\deg(X - a) = 1$.
Polynomial.natDegree_X_sub_C theorem
(x : R) : (X - C x).natDegree = 1
Full source 
theorem natDegree_X_sub_C (x : R) : (X - C x).natDegree = 1 := by
  rw [natDegree_sub_C, natDegree_X]
Natural Degree of Linear Polynomial: $\text{natDegree}(X - x) = 1$
Informal description
For any element $x$ in a ring $R$, the natural degree of the polynomial $X - x$ is equal to $1$, i.e., $\text{natDegree}(X - x) = 1$.
Polynomial.nextCoeff_X_sub_C theorem
[Ring S] (c : S) : nextCoeff (X - C c) = -c
Full source 
@[simp]
theorem nextCoeff_X_sub_C [Ring S] (c : S) : nextCoeff (X - C c) = -c := by
  rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]
Next Coefficient of Linear Polynomial: $\text{nextCoeff}(X - c) = -c$
Informal description
For any element $c$ in a ring $S$, the next coefficient (i.e., the coefficient of $X^0$) of the polynomial $X - c$ is equal to $-c$.
Polynomial.degree_X_pow_sub_C theorem
{n : ℕ} (hn : 0 < n) (a : R) : degree ((X : R[X]) ^ n - C a) = n
Full source 
theorem degree_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) : degree ((X : R[X]) ^ n - C a) = n := by
  rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]
Degree of $X^n - a$ is $n$ for $n > 0$
Informal description
For any positive natural number $n$ and any element $a$ in a ring $R$, the degree of the polynomial $X^n - a$ is equal to $n$, i.e., $\deg(X^n - a) = n$.
Polynomial.X_pow_sub_C_ne_zero theorem
{n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n - C a ≠ 0
Full source 
theorem X_pow_sub_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n - C a ≠ 0 := by
  rw [sub_eq_add_neg, ← map_neg C a]
  exact X_pow_add_C_ne_zero hn _
Non-vanishing of $X^n - a$ for $n > 0$
Informal description
For any positive natural number $n$ and any element $a$ in a ring $R$, the polynomial $X^n - a$ is not equal to the zero polynomial, i.e., $X^n - a \neq 0$.
Polynomial.zero_nmem_multiset_map_X_sub_C theorem
{α : Type*} (m : Multiset α) (f : α → R) : (0 : R[X]) ∉ m.map fun a => X - C (f a)
Full source 
theorem zero_nmem_multiset_map_X_sub_C {α : Type*} (m : Multiset α) (f : α → R) :
    (0 : R[X]) ∉ m.map fun a => X - C (f a) := fun mem =>
  let ⟨_a, _, ha⟩ := Multiset.mem_map.mp mem
  X_sub_C_ne_zero _ ha
Non-membership of Zero in Multiset of Polynomials $X - f(a)$
Informal description
For any multiset $m$ over a type $\alpha$ and any function $f \colon \alpha \to R$, the zero polynomial $0$ is not an element of the multiset obtained by mapping each $a \in m$ to the polynomial $X - C(f(a))$.
Polynomial.natDegree_X_pow_sub_C theorem
{n : ℕ} {r : R} : (X ^ n - C r).natDegree = n
Full source 
theorem natDegree_X_pow_sub_C {n : ℕ} {r : R} : (X ^ n - C r).natDegree = n := by
  rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]
Degree of $X^n - r$ is $n$
Informal description
For any natural number $n$ and any element $r$ in a ring $R$, the degree of the polynomial $X^n - r$ is equal to $n$, i.e., $\deg(X^n - r) = n$.
Polynomial.leadingCoeff_X_sub_C theorem
[Ring S] (r : S) : (X - C r).leadingCoeff = 1
Full source 
@[simp]
theorem leadingCoeff_X_sub_C [Ring S] (r : S) : (X - C r).leadingCoeff = 1 := by
  rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]
Leading Coefficient of $X - r$ is $1$
Informal description
For any element $r$ in a ring $S$, the leading coefficient of the polynomial $X - r$ is equal to $1$, i.e., $\text{lead}(X - r) = 1$.