doc-next-gen

Mathlib.Algebra.Polynomial.Degree.Definitions

Module docstring

{"# Degree of univariate polynomials

Main definitions

  • Polynomial.degree: the degree of a polynomial, where 0 has degree ⊥
  • Polynomial.natDegree: the degree of a polynomial, where 0 has degree 0
  • Polynomial.leadingCoeff: the leading coefficient of a polynomial
  • Polynomial.Monic: a polynomial is monic if its leading coefficient is 0
  • Polynomial.nextCoeff: the next coefficient after the leading coefficient

Main results

  • Polynomial.degree_eq_natDegree: the degree and natDegree coincide for nonzero polynomials "}
Polynomial.degree definition
(p : R[X]) : WithBot ℕ
Full source 
/-- `degree p` is the degree of the polynomial `p`, i.e. the largest `X`-exponent in `p`.
`degree p = some n` when `p ≠ 0` and `n` is the highest power of `X` that appears in `p`, otherwise
`degree 0 = ⊥`. -/
def degree (p : R[X]) : WithBot ℕ :=
  p.support.max
Degree of a polynomial
Informal description
The degree of a polynomial \( p \in R[X] \) is the largest exponent \( n \) such that the coefficient of \( X^n \) in \( p \) is nonzero. If \( p \) is the zero polynomial, its degree is defined as \( \bot \) (the bottom element of `WithBot ℕ`). More formally, for a nonzero polynomial \( p \), the degree is the maximum element of the support of \( p \) (the set of exponents with nonzero coefficients), viewed in `WithBot ℕ`. For the zero polynomial, the support is empty, and the degree is \( \bot \).
Polynomial.natDegree definition
(p : R[X]) : ℕ
Full source 
/-- `natDegree p` forces `degree p` to ℕ, by defining `natDegree 0 = 0`. -/
def natDegree (p : R[X]) : ℕ :=
  (degree p).unbotD 0
Natural degree of a polynomial
Informal description
The natural degree of a polynomial \( p \in R[X] \) is the largest exponent \( n \) such that the coefficient of \( X^n \) in \( p \) is nonzero, with the zero polynomial having degree \( 0 \). More formally, for a nonzero polynomial \( p \), the natural degree is the maximum element of the support of \( p \) (the set of exponents with nonzero coefficients). For the zero polynomial, the natural degree is defined as \( 0 \).
Polynomial.leadingCoeff definition
(p : R[X]) : R
Full source 
/-- `leadingCoeff p` gives the coefficient of the highest power of `X` in `p`. -/
def leadingCoeff (p : R[X]) : R :=
  coeff p (natDegree p)
Leading coefficient of a polynomial
Informal description
The leading coefficient of a polynomial \( p \in R[X] \) is the coefficient of the highest power term \( X^n \) in \( p \), where \( n \) is the natural degree of \( p \). More formally, for a polynomial \( p \), the leading coefficient is given by \( p_n \), where \( n \) is the largest exponent such that \( p_n \neq 0 \). If \( p \) is the zero polynomial, the leading coefficient is \( 0 \).
Polynomial.Monic definition
(p : R[X])
Full source 
/-- a polynomial is `Monic` if its leading coefficient is 1 -/
def Monic (p : R[X]) :=
  leadingCoeff p = (1 : R)
Monic polynomial
Informal description
A polynomial \( p \in R[X] \) is called *monic* if its leading coefficient is equal to the multiplicative identity \( 1 \) of the semiring \( R \).
Polynomial.Monic.def theorem
: Monic p ↔ leadingCoeff p = 1
Full source 
theorem Monic.def : MonicMonic p ↔ leadingCoeff p = 1 :=
  Iff.rfl
Characterization of Monic Polynomials via Leading Coefficient
Informal description
A polynomial $p \in R[X]$ is monic if and only if its leading coefficient is equal to $1$, i.e., $\text{leadingCoeff}(p) = 1$.
Polynomial.Monic.decidable instance
[DecidableEq R] : Decidable (Monic p)
Full source 
instance Monic.decidable [DecidableEq R] : Decidable (Monic p) := by unfold Monic; infer_instance
Decidability of Monic Polynomials
Informal description
For any semiring $R$ with decidable equality, the property of a polynomial $p \in R[X]$ being monic (i.e., having leading coefficient equal to $1$) is decidable.
Polynomial.Monic.leadingCoeff theorem
{p : R[X]} (hp : p.Monic) : leadingCoeff p = 1
Full source 
@[simp]
theorem Monic.leadingCoeff {p : R[X]} (hp : p.Monic) : leadingCoeff p = 1 :=
  hp
Leading coefficient of a monic polynomial is 1
Informal description
For any monic polynomial $p \in R[X]$, the leading coefficient of $p$ is equal to $1$.
Polynomial.Monic.coeff_natDegree theorem
{p : R[X]} (hp : p.Monic) : p.coeff p.natDegree = 1
Full source 
theorem Monic.coeff_natDegree {p : R[X]} (hp : p.Monic) : p.coeff p.natDegree = 1 :=
  hp
Leading Coefficient of Monic Polynomial is One
Informal description
For any monic polynomial $p \in R[X]$, the coefficient of the term $X^{\operatorname{natDegree}(p)}$ is equal to $1$, i.e., $p_{\operatorname{natDegree}(p)} = 1$.
Polynomial.degree_zero theorem
: degree (0 : R[X]) = ⊥
Full source 
@[simp]
theorem degree_zero : degree (0 : R[X]) = ⊥ :=
  rfl
Degree of Zero Polynomial is Bottom
Informal description
The degree of the zero polynomial in $R[X]$ is equal to the bottom element $\bot$ of the type `WithBot ℕ}$.
Polynomial.natDegree_zero theorem
: natDegree (0 : R[X]) = 0
Full source 
@[simp]
theorem natDegree_zero : natDegree (0 : R[X]) = 0 :=
  rfl
Natural Degree of Zero Polynomial is Zero
Informal description
For the zero polynomial $0 \in R[X]$, the natural degree is $0$.
Polynomial.coeff_natDegree theorem
: coeff p (natDegree p) = leadingCoeff p
Full source 
@[simp]
theorem coeff_natDegree : coeff p (natDegree p) = leadingCoeff p :=
  rfl
Coefficient at Natural Degree Equals Leading Coefficient
Informal description
For any polynomial $p \in R[X]$, the coefficient of the term $X^n$ where $n$ is the natural degree of $p$ is equal to the leading coefficient of $p$, i.e., $p_n = \text{leadingCoeff}(p)$.
Polynomial.degree_eq_natDegree theorem
(hp : p ≠ 0) : degree p = (natDegree p : WithBot ℕ)
Full source 
theorem degree_eq_natDegree (hp : p ≠ 0) : degree p = (natDegree p : WithBot ℕ) := by
  let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt degree_eq_bot.1 hp))
  have hn : degree p = some n := Classical.not_not.1 hn
  rw [natDegree, hn]; rfl
Degree and Natural Degree Coincide for Nonzero Polynomials
Informal description
For any nonzero polynomial $p \in R[X]$, the degree of $p$ (as an element of `WithBot ℕ`) is equal to its natural degree (as a natural number), i.e., $\text{degree}(p) = \text{natDegree}(p)$.
Polynomial.degree_eq_iff_natDegree_eq theorem
{p : R[X]} {n : ℕ} (hp : p ≠ 0) : p.degree = n ↔ p.natDegree = n
Full source 
theorem degree_eq_iff_natDegree_eq {p : R[X]} {n : ℕ} (hp : p ≠ 0) :
    p.degree = n ↔ p.natDegree = n := by rw [degree_eq_natDegree hp]; exact WithBot.coe_eq_coe
Equivalence of Degree and Natural Degree for Nonzero Polynomials
Informal description
For any nonzero polynomial $p \in R[X]$ and any natural number $n$, the degree of $p$ is equal to $n$ if and only if the natural degree of $p$ is equal to $n$. That is, $\deg(p) = n \leftrightarrow \text{natDegree}(p) = n$.
Polynomial.degree_eq_iff_natDegree_eq_of_pos theorem
{p : R[X]} {n : ℕ} (hn : 0 < n) : p.degree = n ↔ p.natDegree = n
Full source 
theorem degree_eq_iff_natDegree_eq_of_pos {p : R[X]} {n : ℕ} (hn : 0 < n) :
    p.degree = n ↔ p.natDegree = n := by
  obtain rfl|h := eq_or_ne p 0
  · simp [hn.ne]
  · exact degree_eq_iff_natDegree_eq h
Equivalence of Degree and Natural Degree for Nonzero Polynomials with Positive Degree
Informal description
For any polynomial $p \in R[X]$ and positive natural number $n > 0$, the degree of $p$ is equal to $n$ if and only if the natural degree of $p$ is equal to $n$. That is, $\deg(p) = n \leftrightarrow \text{natDegree}(p) = n$.
Polynomial.natDegree_eq_of_degree_eq_some theorem
{p : R[X]} {n : ℕ} (h : degree p = n) : natDegree p = n
Full source 
theorem natDegree_eq_of_degree_eq_some {p : R[X]} {n : ℕ} (h : degree p = n) : natDegree p = n := by
  rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]
Equality of Natural Degree When Degree is Given as a Natural Number
Informal description
For any polynomial $p \in R[X]$ and natural number $n$, if the degree of $p$ is equal to $n$ (viewed in `WithBot ℕ`), then the natural degree of $p$ is also equal to $n$.
Polynomial.degree_le_natDegree theorem
: degree p ≤ natDegree p
Full source 
@[simp]
theorem degree_le_natDegree : degree p ≤ natDegree p :=
  WithBot.giUnbotDBot.gc.le_u_l _
Degree Bounded by Natural Degree for Polynomials
Informal description
For any polynomial $p \in R[X]$, the degree of $p$ (with $\bot$ for the zero polynomial) is less than or equal to its natural degree (with $0$ for the zero polynomial). In other words, $\deg(p) \leq \text{natDegree}(p)$.
Polynomial.natDegree_eq_of_degree_eq theorem
[Semiring S] {q : S[X]} (h : degree p = degree q) : natDegree p = natDegree q
Full source 
theorem natDegree_eq_of_degree_eq [Semiring S] {q : S[X]} (h : degree p = degree q) :
    natDegree p = natDegree q := by unfold natDegree; rw [h]
Equality of Natural Degrees from Equality of Degrees
Informal description
Let $R$ and $S$ be semirings, and let $p \in R[X]$ and $q \in S[X]$ be polynomials. If the degrees of $p$ and $q$ are equal, then their natural degrees are also equal. That is, if $\deg(p) = \deg(q)$, then $\text{natDegree}(p) = \text{natDegree}(q)$.
Polynomial.le_degree_of_ne_zero theorem
(h : coeff p n ≠ 0) : (n : WithBot ℕ) ≤ degree p
Full source 
theorem le_degree_of_ne_zero (h : coeffcoeff p n ≠ 0) : (n : WithBot ℕ) ≤ degree p := by
  rw [Nat.cast_withBot]
  exact Finset.le_sup (mem_support_iff.2 h)
Nonzero Coefficients Imply Exponent Bounded by Degree: $n \leq \deg(p)$ for $p_n \neq 0$
Informal description
For a polynomial $p \in R[X]$ and a natural number $n$, if the coefficient of $X^n$ in $p$ is nonzero, then $n$ is less than or equal to the degree of $p$ (viewed in `WithBot ℕ`). In other words, if $p_n \neq 0$, then $n \leq \deg(p)$.
Polynomial.degree_mono theorem
[Semiring S] {f : R[X]} {g : S[X]} (h : f.support ⊆ g.support) : f.degree ≤ g.degree
Full source 
theorem degree_mono [Semiring S] {f : R[X]} {g : S[X]} (h : f.support ⊆ g.support) :
    f.degree ≤ g.degree :=
  Finset.sup_mono h
Monotonicity of Polynomial Degree under Support Inclusion
Informal description
Let $R$ and $S$ be semirings, and let $f \in R[X]$ and $g \in S[X]$ be polynomials. If the support of $f$ (the set of exponents with nonzero coefficients) is contained in the support of $g$, then the degree of $f$ is less than or equal to the degree of $g$. That is, if $\operatorname{supp}(f) \subseteq \operatorname{supp}(g)$, then $\deg(f) \leq \deg(g)$.
Polynomial.degree_le_degree theorem
(h : coeff q (natDegree p) ≠ 0) : degree p ≤ degree q
Full source 
theorem degree_le_degree (h : coeffcoeff q (natDegree p) ≠ 0) : degree p ≤ degree q := by
  by_cases hp : p = 0
  · rw [hp, degree_zero]
    exact bot_le
  · rw [degree_eq_natDegree hp]
    exact le_degree_of_ne_zero h
Degree Comparison via Leading Coefficient: $\deg(p) \leq \deg(q)$ when $q_{\deg(p)} \neq 0$
Informal description
For polynomials $p, q \in R[X]$, if the coefficient of $X^{\text{natDegree}(p)}$ in $q$ is nonzero, then the degree of $p$ is less than or equal to the degree of $q$, i.e., $\deg(p) \leq \deg(q)$.
Polynomial.natDegree_le_iff_degree_le theorem
{n : ℕ} : natDegree p ≤ n ↔ degree p ≤ n
Full source 
theorem natDegree_le_iff_degree_le {n : ℕ} : natDegreenatDegree p ≤ n ↔ degree p ≤ n :=
  WithBot.unbotD_le_iff (fun _ ↦ bot_le)
Equivalence of Natural Degree and Degree Bounds for Polynomials
Informal description
For any polynomial $p \in R[X]$ and any natural number $n$, the natural degree of $p$ is less than or equal to $n$ if and only if the degree of $p$ (as an element of $\mathbb{N} \cup \{\bot\}$) is less than or equal to $n$.
Polynomial.natDegree_lt_iff_degree_lt theorem
(hp : p ≠ 0) : p.natDegree < n ↔ p.degree < ↑n
Full source 
theorem natDegree_lt_iff_degree_lt (hp : p ≠ 0) : p.natDegree < n ↔ p.degree < ↑n :=
  WithBot.unbotD_lt_iff (absurd · (degree_eq_bot.not.mpr hp))
Equivalence of Natural Degree and Degree Strict Bounds for Nonzero Polynomials
Informal description
For a nonzero polynomial $p \in R[X]$ and a natural number $n$, the natural degree of $p$ is less than $n$ if and only if the degree of $p$ (as an element of $\mathbb{N} \cup \{\bot\}$) is less than $n$.
Polynomial.natDegree_le_natDegree theorem
[Semiring S] {q : S[X]} (hpq : p.degree ≤ q.degree) : p.natDegree ≤ q.natDegree
Full source 
theorem natDegree_le_natDegree [Semiring S] {q : S[X]} (hpq : p.degree ≤ q.degree) :
    p.natDegree ≤ q.natDegree :=
  WithBot.giUnbotDBot.gc.monotone_l hpq
Natural Degree Comparison via Degree Inequality
Informal description
For polynomials $p$ over a semiring $R$ and $q$ over a semiring $S$, if the degree of $p$ is less than or equal to the degree of $q$, then the natural degree of $p$ is less than or equal to the natural degree of $q$.
Polynomial.degree_C_le theorem
: degree (C a) ≤ 0
Full source 
theorem degree_C_le : degree (C a) ≤ 0 := by
  by_cases h : a = 0
  · rw [h, C_0]
    exact bot_le
  · rw [degree_C h]
Degree Bound for Constant Polynomials: $\deg(C(a)) \leq 0$
Informal description
For any element $a$ in a semiring $R$, the degree of the constant polynomial $C(a) \in R[X]$ is less than or equal to $0$.
Polynomial.degree_C_lt theorem
: degree (C a) < 1
Full source 
theorem degree_C_lt : degree (C a) < 1 :=
  degree_C_le.trans_lt <| WithBot.coe_lt_coe.mpr zero_lt_one
Degree Bound for Constant Polynomials: $\deg(C(a)) < 1$
Informal description
For any element $a$ in a semiring $R$, the degree of the constant polynomial $C(a) \in R[X]$ is strictly less than $1$.
Polynomial.degree_one_le theorem
: degree (1 : R[X]) ≤ (0 : WithBot ℕ)
Full source 
theorem degree_one_le : degree (1 : R[X]) ≤ (0 : WithBot ℕ) := by rw [← C_1]; exact degree_C_le
Degree Bound for the Unit Polynomial: $\deg(1) \leq 0$
Informal description
For the constant polynomial $1 \in R[X]$, the degree satisfies $\deg(1) \leq 0$.
Polynomial.natDegree_one theorem
: natDegree (1 : R[X]) = 0
Full source 
@[simp]
theorem natDegree_one : natDegree (1 : R[X]) = 0 :=
  natDegree_C 1
Natural Degree of the Unit Polynomial is Zero
Informal description
The natural degree of the constant polynomial $1$ in the polynomial ring $R[X]$ is $0$.
Polynomial.natDegree_natCast theorem
(n : ℕ) : natDegree (n : R[X]) = 0
Full source 
@[simp]
theorem natDegree_natCast (n : ℕ) : natDegree (n : R[X]) = 0 := by
  simp only [← C_eq_natCast, natDegree_C]
Natural degree of constant polynomial from natural number is zero
Informal description
For any natural number $n$, the natural degree of the constant polynomial $n$ in the polynomial ring $R[X]$ is $0$.
Polynomial.natDegree_ofNat theorem
(n : ℕ) [Nat.AtLeastTwo n] : natDegree (ofNat(n) : R[X]) = 0
Full source 
@[simp]
theorem natDegree_ofNat (n : ℕ) [Nat.AtLeastTwo n] :
    natDegree (ofNat(n) : R[X]) = 0 :=
  natDegree_natCast _
Natural Degree of Constant Polynomial from Numerals ≥ 2 is Zero
Informal description
For any natural number $n \geq 2$, the natural degree of the constant polynomial $n$ in the polynomial ring $R[X]$ is $0$.
Polynomial.degree_natCast_le theorem
(n : ℕ) : degree (n : R[X]) ≤ 0
Full source 
theorem degree_natCast_le (n : ℕ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp)
Degree Bound for Constant Polynomials from Natural Numbers
Informal description
For any natural number $n$, the degree of the constant polynomial $n$ in the polynomial ring $R[X]$ is less than or equal to $0$.
Polynomial.degree_monomial theorem
(n : ℕ) (ha : a ≠ 0) : degree (monomial n a) = n
Full source 
@[simp]
theorem degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (monomial n a) = n := by
  rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]
Degree of monomial $a X^n$ is $n$ for $a \neq 0$
Informal description
For any natural number $n$ and nonzero element $a$ in a semiring $R$, the degree of the monomial $a X^n$ is equal to $n$.
Polynomial.degree_C_mul_X_pow theorem
(n : ℕ) (ha : a ≠ 0) : degree (C a * X ^ n) = n
Full source 
@[simp]
theorem degree_C_mul_X_pow (n : ℕ) (ha : a ≠ 0) : degree (C a * X ^ n) = n := by
  rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]
Degree of Monomial $a X^n$ is $n$ for $a \neq 0$
Informal description
For any natural number $n$ and nonzero element $a$ in a semiring $R$, the degree of the polynomial $a X^n$ is equal to $n$. In mathematical notation: $$\deg(a X^n) = n \quad \text{for } a \neq 0.$$
Polynomial.degree_C_mul_X theorem
(ha : a ≠ 0) : degree (C a * X) = 1
Full source 
theorem degree_C_mul_X (ha : a ≠ 0) : degree (C a * X) = 1 := by
  simpa only [pow_one] using degree_C_mul_X_pow 1 ha
Degree of Linear Monomial: $\deg(a X) = 1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a semiring $R$, the degree of the polynomial $a X$ is equal to $1$, i.e., $\deg(a X) = 1$.
Polynomial.degree_monomial_le theorem
(n : ℕ) (a : R) : degree (monomial n a) ≤ n
Full source 
theorem degree_monomial_le (n : ℕ) (a : R) : degree (monomial n a) ≤ n :=
  letI := Classical.decEq R
  if h : a = 0 then by rw [h, (monomial n).map_zero, degree_zero]; exact bot_le
  else le_of_eq (degree_monomial n h)
Degree Bound for Monomials: $\deg(a X^n) \leq n$
Informal description
For any natural number $n$ and coefficient $a$ in a semiring $R$, the degree of the monomial $a X^n$ is less than or equal to $n$. More precisely, if $a \neq 0$, then the degree is exactly $n$; if $a = 0$, the degree is $\bot$ (the bottom element of `WithBot ℕ`), which is considered less than or equal to all natural numbers.
Polynomial.degree_C_mul_X_pow_le theorem
(n : ℕ) (a : R) : degree (C a * X ^ n) ≤ n
Full source 
theorem degree_C_mul_X_pow_le (n : ℕ) (a : R) : degree (C a * X ^ n) ≤ n := by
  rw [C_mul_X_pow_eq_monomial]
  apply degree_monomial_le
Degree bound for monomials: $\deg(a X^n) \leq n$
Informal description
For any natural number $n$ and coefficient $a$ in a semiring $R$, the degree of the polynomial $a X^n$ is less than or equal to $n$.
Polynomial.degree_C_mul_X_le theorem
(a : R) : degree (C a * X) ≤ 1
Full source 
theorem degree_C_mul_X_le (a : R) : degree (C a * X) ≤ 1 := by
  simpa only [pow_one] using degree_C_mul_X_pow_le 1 a
Degree bound for linear monomials: $\deg(a X) \leq 1$
Informal description
For any coefficient $a$ in a semiring $R$, the degree of the polynomial $a X$ is less than or equal to $1$.
Polynomial.natDegree_C_mul_X_pow theorem
(n : ℕ) (a : R) (ha : a ≠ 0) : natDegree (C a * X ^ n) = n
Full source 
@[simp]
theorem natDegree_C_mul_X_pow (n : ℕ) (a : R) (ha : a ≠ 0) : natDegree (C a * X ^ n) = n :=
  natDegree_eq_of_degree_eq_some (degree_C_mul_X_pow n ha)
Natural Degree of Monomial $a X^n$ is $n$ for $a \neq 0$
Informal description
For any natural number $n$ and nonzero element $a$ in a semiring $R$, the natural degree of the monomial $a X^n$ is equal to $n$. In mathematical notation: $$\text{natDegree}(a X^n) = n \quad \text{for } a \neq 0.$$
Polynomial.natDegree_C_mul_X theorem
(a : R) (ha : a ≠ 0) : natDegree (C a * X) = 1
Full source 
@[simp]
theorem natDegree_C_mul_X (a : R) (ha : a ≠ 0) : natDegree (C a * X) = 1 := by
  simpa only [pow_one] using natDegree_C_mul_X_pow 1 a ha
Natural Degree of Linear Monomial $a X$ is $1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a semiring $R$, the natural degree of the polynomial $a X$ is equal to $1$, i.e., $$\text{natDegree}(a X) = 1 \quad \text{for } a \neq 0.$$
Polynomial.natDegree_monomial theorem
[DecidableEq R] (i : ℕ) (r : R) : natDegree (monomial i r) = if r = 0 then 0 else i
Full source 
@[simp]
theorem natDegree_monomial [DecidableEq R] (i : ℕ) (r : R) :
    natDegree (monomial i r) = if r = 0 then 0 else i := by
  split_ifs with hr
  · simp [hr]
  · rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]
Natural Degree of Monomial: $\text{natDegree}(r X^i) = \text{if } r = 0 \text{ then } 0 \text{ else } i$
Informal description
For any natural number $i$ and element $r$ in a semiring $R$ with decidable equality, the natural degree of the monomial $r X^i$ is equal to $0$ if $r = 0$, and $i$ otherwise. In mathematical notation: $$\text{natDegree}(r X^i) = \begin{cases} 0 & \text{if } r = 0, \\ i & \text{otherwise.} \end{cases}$$
Polynomial.natDegree_monomial_le theorem
(a : R) {m : ℕ} : (monomial m a).natDegree ≤ m
Full source 
theorem natDegree_monomial_le (a : R) {m : ℕ} : (monomial m a).natDegree ≤ m := by
  classical
  rw [Polynomial.natDegree_monomial]
  split_ifs
  exacts [Nat.zero_le _, le_rfl]
Upper Bound on Natural Degree of Monomial: $\text{natDegree}(a X^m) \leq m$
Informal description
For any coefficient $a$ in a semiring $R$ and any natural number $m$, the natural degree of the monomial $a X^m$ is less than or equal to $m$.
Polynomial.natDegree_monomial_eq theorem
(i : ℕ) {r : R} (r0 : r ≠ 0) : (monomial i r).natDegree = i
Full source 
theorem natDegree_monomial_eq (i : ℕ) {r : R} (r0 : r ≠ 0) : (monomial i r).natDegree = i :=
  letI := Classical.decEq R
  Eq.trans (natDegree_monomial _ _) (if_neg r0)
Natural Degree of Nonzero Monomial: $\text{natDegree}(r X^i) = i$ for $r \neq 0$
Informal description
For any natural number $i$ and nonzero element $r$ in a semiring $R$, the natural degree of the monomial $r X^i$ is equal to $i$.
Polynomial.coeff_ne_zero_of_eq_degree theorem
(hn : degree p = n) : coeff p n ≠ 0
Full source 
theorem coeff_ne_zero_of_eq_degree (hn : degree p = n) : coeffcoeff p n ≠ 0 := fun h =>
  mem_support_iff.mp (mem_of_max hn) h
Nonzero Leading Coefficient for Polynomial of Degree $n$
Informal description
For a polynomial $p \in R[X]$ and a natural number $n$, if the degree of $p$ is equal to $n$, then the coefficient of $X^n$ in $p$ is nonzero.
Polynomial.degree_X_pow_le theorem
(n : ℕ) : degree (X ^ n : R[X]) ≤ n
Full source 
theorem degree_X_pow_le (n : ℕ) : degree (X ^ n : R[X]) ≤ n := by
  simpa only [C_1, one_mul] using degree_C_mul_X_pow_le n (1 : R)
Degree Bound for Powers of $X$: $\deg(X^n) \leq n$
Informal description
For any natural number $n$, the degree of the polynomial $X^n$ in the polynomial ring $R[X]$ is less than or equal to $n$, i.e., $\deg(X^n) \leq n$.
Polynomial.degree_X_le theorem
: degree (X : R[X]) ≤ 1
Full source 
theorem degree_X_le : degree (X : R[X]) ≤ 1 :=
  degree_monomial_le _ _
Degree Bound for Polynomial Variable: $\deg(X) \leq 1$
Informal description
For the polynomial variable $X$ in the polynomial ring $R[X]$, the degree of $X$ is less than or equal to $1$, i.e., $\deg(X) \leq 1$.
Polynomial.natDegree_X_le theorem
: (X : R[X]).natDegree ≤ 1
Full source 
theorem natDegree_X_le : (X : R[X]).natDegree ≤ 1 :=
  natDegree_le_of_degree_le degree_X_le
Natural Degree Bound for Polynomial Variable: $\text{natDegree}(X) \leq 1$
Informal description
For the polynomial variable $X$ in the polynomial ring $R[X]$, the natural degree of $X$ is less than or equal to $1$, i.e., $\text{natDegree}(X) \leq 1$.
Polynomial.withBotSucc_degree_eq_natDegree_add_one theorem
(h : p ≠ 0) : p.degree.succ = p.natDegree + 1
Full source 
theorem withBotSucc_degree_eq_natDegree_add_one (h : p ≠ 0) : p.degree.succ = p.natDegree + 1 := by
  rw [degree_eq_natDegree h]
  exact WithBot.succ_coe p.natDegree
Successor of Degree Equals Natural Degree Plus One for Nonzero Polynomials
Informal description
For any nonzero polynomial $p \in R[X]$, the successor of its degree (in `WithBot ℕ`) is equal to its natural degree plus one, i.e., $\text{degree}(p).\text{succ} = \text{natDegree}(p) + 1$.
Polynomial.degree_one theorem
: degree (1 : R[X]) = (0 : WithBot ℕ)
Full source 
@[simp]
theorem degree_one : degree (1 : R[X]) = (0 : WithBot ℕ) :=
  degree_C one_ne_zero
Degree of the Constant One Polynomial is Zero
Informal description
The degree of the constant polynomial $1 \in R[X]$ is $0$.
Polynomial.degree_X theorem
: degree (X : R[X]) = 1
Full source 
@[simp]
theorem degree_X : degree (X : R[X]) = 1 :=
  degree_monomial _ one_ne_zero
Degree of $X$ is $1$
Informal description
The degree of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to $1$.
Polynomial.natDegree_X theorem
: (X : R[X]).natDegree = 1
Full source 
@[simp]
theorem natDegree_X : (X : R[X]).natDegree = 1 :=
  natDegree_eq_of_degree_eq_some degree_X
Natural Degree of $X$ is $1$ in Polynomial Ring $R[X]$
Informal description
For any nontrivial semiring $R$, the natural degree of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to $1$.
Polynomial.degree_neg theorem
(p : R[X]) : degree (-p) = degree p
Full source 
@[simp]
theorem degree_neg (p : R[X]) : degree (-p) = degree p := by unfold degree; rw [support_neg]
Degree Invariance under Negation: $\deg(-p) = \deg(p)$
Informal description
For any polynomial $p \in R[X]$ over a ring $R$, the degree of the negated polynomial $-p$ is equal to the degree of $p$.
Polynomial.degree_neg_le_of_le theorem
{a : WithBot ℕ} {p : R[X]} (hp : degree p ≤ a) : degree (-p) ≤ a
Full source 
theorem degree_neg_le_of_le {a : WithBot ℕ} {p : R[X]} (hp : degree p ≤ a) : degree (-p) ≤ a :=
  p.degree_neg.le.trans hp
Degree Upper Bound Preservation under Negation: $\deg(-p) \leq a$ if $\deg(p) \leq a$
Informal description
For any polynomial $p \in R[X]$ over a ring $R$ and any upper bound $a \in \text{WithBot }\mathbb{N}$, if the degree of $p$ is less than or equal to $a$, then the degree of $-p$ is also less than or equal to $a$.
Polynomial.natDegree_neg theorem
(p : R[X]) : natDegree (-p) = natDegree p
Full source 
@[simp]
theorem natDegree_neg (p : R[X]) : natDegree (-p) = natDegree p := by simp [natDegree]
Natural Degree Invariance under Negation: $\text{natDegree}(-p) = \text{natDegree}(p)$
Informal description
For any polynomial $p \in R[X]$ over a ring $R$, the natural degree of the negated polynomial $-p$ is equal to the natural degree of $p$, i.e., $\text{natDegree}(-p) = \text{natDegree}(p)$.
Polynomial.natDegree_neg_le_of_le theorem
{p : R[X]} (hp : natDegree p ≤ m) : natDegree (-p) ≤ m
Full source 
theorem natDegree_neg_le_of_le {p : R[X]} (hp : natDegree p ≤ m) : natDegree (-p) ≤ m :=
  (natDegree_neg p).le.trans hp
Natural Degree Upper Bound Preservation under Negation: $\text{natDegree}(-p) \leq m$ if $\text{natDegree}(p) \leq m$
Informal description
For any polynomial $p \in R[X]$ over a ring $R$ and any natural number $m$, if the natural degree of $p$ is at most $m$, then the natural degree of $-p$ is also at most $m$.
Polynomial.natDegree_intCast theorem
(n : ℤ) : natDegree (n : R[X]) = 0
Full source 
@[simp]
theorem natDegree_intCast (n : ℤ) : natDegree (n : R[X]) = 0 := by
  rw [← C_eq_intCast, natDegree_C]
Natural Degree of Integer Cast Polynomial is Zero
Informal description
For any integer $n \in \mathbb{Z}$, the natural degree of the polynomial obtained by casting $n$ into the polynomial ring $R[X]$ is $0$.
Polynomial.degree_intCast_le theorem
(n : ℤ) : degree (n : R[X]) ≤ 0
Full source 
theorem degree_intCast_le (n : ℤ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp)
Degree Bound for Integer Polynomials: $\deg(n) \leq 0$
Informal description
For any integer $n \in \mathbb{Z}$, the degree of the constant polynomial $n$ in $R[X]$ is at most $0$.
Polynomial.leadingCoeff_neg theorem
(p : R[X]) : (-p).leadingCoeff = -p.leadingCoeff
Full source 
@[simp]
theorem leadingCoeff_neg (p : R[X]) : (-p).leadingCoeff = -p.leadingCoeff := by
  rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
Negation of Leading Coefficient: $\text{lc}(-p) = -\text{lc}(p)$
Informal description
For any polynomial $p \in R[X]$ over a ring $R$, the leading coefficient of the negated polynomial $-p$ is equal to the negation of the leading coefficient of $p$, i.e., $$ \text{leadingCoeff}(-p) = -\text{leadingCoeff}(p). $$
Polynomial.nextCoeff definition
(p : R[X]) : R
Full source 
/-- The second-highest coefficient, or 0 for constants -/
def nextCoeff (p : R[X]) : R :=
  if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)
Next coefficient of a polynomial
Informal description
For a polynomial \( p \in R[X] \), the next coefficient after the leading coefficient is defined as follows: if \( p \) is a constant polynomial (i.e., \( \text{natDegree}(p) = 0 \)), then the next coefficient is \( 0 \); otherwise, it is the coefficient of the term \( X^{\text{natDegree}(p) - 1} \).
Polynomial.nextCoeff_eq_zero theorem
: p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0
Full source 
lemma nextCoeff_eq_zero :
    p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0 := by
  simp [nextCoeff, or_iff_not_imp_left, pos_iff_ne_zero]; aesop
Characterization of Zero Next Coefficient in Polynomials
Informal description
For a polynomial $p \in R[X]$, the next coefficient after the leading coefficient is zero if and only if either: 1. $p$ has degree zero (i.e., $p$ is a constant polynomial), or 2. $p$ has positive degree and the coefficient of $X^{\text{natDegree}(p) - 1}$ is zero. In symbols: \[ \text{nextCoeff}(p) = 0 \leftrightarrow \text{natDegree}(p) = 0 \lor \left(0 < \text{natDegree}(p) \land \text{coeff}(p, \text{natDegree}(p) - 1) = 0\right) \]
Polynomial.nextCoeff_ne_zero theorem
: p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0
Full source 
lemma nextCoeff_ne_zero : p.nextCoeff ≠ 0p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0 := by
  simp [nextCoeff]
Nonzero Next Coefficient Condition for Polynomials
Informal description
For a polynomial $p \in R[X]$, the next coefficient after the leading coefficient is nonzero if and only if $p$ is not a constant polynomial (i.e., its natural degree is not zero) and the coefficient of the term $X^{\text{natDegree}(p) - 1}$ is nonzero. In other words, $p.\text{nextCoeff} \neq 0$ if and only if $p.\text{natDegree} \neq 0$ and $p.\text{coeff}(\text{natDegree}(p) - 1) \neq 0$.
Polynomial.nextCoeff_C_eq_zero theorem
(c : R) : nextCoeff (C c) = 0
Full source 
@[simp]
theorem nextCoeff_C_eq_zero (c : R) : nextCoeff (C c) = 0 := by
  rw [nextCoeff]
  simp
Next coefficient of a constant polynomial is zero
Informal description
For any element $c$ in a semiring $R$, the next coefficient after the leading coefficient of the constant polynomial $C(c) \in R[X]$ is zero.
Polynomial.nextCoeff_of_natDegree_pos theorem
(hp : 0 < p.natDegree) : nextCoeff p = p.coeff (p.natDegree - 1)
Full source 
theorem nextCoeff_of_natDegree_pos (hp : 0 < p.natDegree) :
    nextCoeff p = p.coeff (p.natDegree - 1) := by
  rw [nextCoeff, if_neg]
  contrapose! hp
  simpa
Next coefficient formula for polynomials with positive degree
Informal description
For a polynomial $p \in R[X]$ with positive natural degree (i.e., $\text{natDegree}(p) > 0$), the next coefficient after the leading coefficient is equal to the coefficient of the term $X^{\text{natDegree}(p)-1}$ in $p$.
Polynomial.degree_add_le theorem
(p q : R[X]) : degree (p + q) ≤ max (degree p) (degree q)
Full source 
theorem degree_add_le (p q : R[X]) : degree (p + q) ≤ max (degree p) (degree q) := by
  simpa only [degree, ← support_toFinsupp, toFinsupp_add]
    using AddMonoidAlgebra.sup_support_add_le _ _ _
Degree Bound for Sum of Polynomials: $\deg(p + q) \leq \max(\deg p, \deg q)$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, the degree of their sum satisfies $\deg(p + q) \leq \max(\deg p, \deg q)$, where $\deg$ denotes the polynomial degree (with $\deg 0 = \bot$).
Polynomial.degree_add_le_of_degree_le theorem
{p q : R[X]} {n : ℕ} (hp : degree p ≤ n) (hq : degree q ≤ n) : degree (p + q) ≤ n
Full source 
theorem degree_add_le_of_degree_le {p q : R[X]} {n : ℕ} (hp : degree p ≤ n) (hq : degree q ≤ n) :
    degree (p + q) ≤ n :=
  (degree_add_le p q).trans <| max_le hp hq
Degree Bound for Sum of Polynomials with Bounded Degrees: $\deg(p + q) \leq n$ when $\deg p, \deg q \leq n$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$ and any natural number $n$, if the degrees of $p$ and $q$ are both bounded above by $n$, then the degree of their sum $p + q$ is also bounded above by $n$.
Polynomial.degree_add_le_of_le theorem
{a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) : degree (p + q) ≤ max a b
Full source 
theorem degree_add_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) :
    degree (p + q) ≤ max a b :=
  (p.degree_add_le q).trans <| max_le_max ‹_› ‹_›
Degree Bound for Sum of Polynomials with Given Degree Bounds: $\deg(p + q) \leq \max(a, b)$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, if the degree of $p$ is at most $a$ and the degree of $q$ is at most $b$ (where $a, b \in \mathbb{N} \cup \{\bot\}$), then the degree of their sum $p + q$ is at most $\max(a, b)$.
Polynomial.natDegree_add_le theorem
(p q : R[X]) : natDegree (p + q) ≤ max (natDegree p) (natDegree q)
Full source 
theorem natDegree_add_le (p q : R[X]) : natDegree (p + q) ≤ max (natDegree p) (natDegree q) := by
  rcases le_max_iff.1 (degree_add_le p q) with h | h <;> simp [natDegree_le_natDegree h]
Natural Degree Bound for Sum of Polynomials: $\mathrm{natDegree}(p + q) \leq \max(\mathrm{natDegree}(p), \mathrm{natDegree}(q))$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, the natural degree of their sum satisfies $\mathrm{natDegree}(p + q) \leq \max(\mathrm{natDegree}(p), \mathrm{natDegree}(q))$.
Polynomial.natDegree_add_le_of_degree_le theorem
{p q : R[X]} {n : ℕ} (hp : natDegree p ≤ n) (hq : natDegree q ≤ n) : natDegree (p + q) ≤ n
Full source 
theorem natDegree_add_le_of_degree_le {p q : R[X]} {n : ℕ} (hp : natDegree p ≤ n)
    (hq : natDegree q ≤ n) : natDegree (p + q) ≤ n :=
  (natDegree_add_le p q).trans <| max_le hp hq
Natural Degree Bound for Sum of Polynomials with Bounded Degrees: $\mathrm{natDegree}(p + q) \leq n$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$ and any natural number $n$, if the natural degrees of $p$ and $q$ are both at most $n$, then the natural degree of their sum $p + q$ is also at most $n$.
Polynomial.natDegree_add_le_of_le theorem
(hp : natDegree p ≤ m) (hq : natDegree q ≤ n) : natDegree (p + q) ≤ max m n
Full source 
theorem natDegree_add_le_of_le (hp : natDegree p ≤ m) (hq : natDegree q ≤ n) :
    natDegree (p + q) ≤ max m n :=
  (p.natDegree_add_le q).trans <| max_le_max ‹_› ‹_›
Natural Degree Bound for Sum of Polynomials: $\mathrm{natDegree}(p + q) \leq \max(m, n)$ under degree constraints
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, if the natural degree of $p$ is at most $m$ and the natural degree of $q$ is at most $n$, then the natural degree of their sum $p + q$ is at most $\max(m, n)$.
Polynomial.leadingCoeff_zero theorem
: leadingCoeff (0 : R[X]) = 0
Full source 
@[simp]
theorem leadingCoeff_zero : leadingCoeff (0 : R[X]) = 0 :=
  rfl
Leading coefficient of zero polynomial is zero
Informal description
The leading coefficient of the zero polynomial in $R[X]$ is equal to $0$.
Polynomial.leadingCoeff_eq_zero theorem
: leadingCoeff p = 0 ↔ p = 0
Full source 
@[simp]
theorem leadingCoeff_eq_zero : leadingCoeffleadingCoeff p = 0 ↔ p = 0 :=
  ⟨fun h =>
    Classical.by_contradiction fun hp =>
      mt mem_support_iff.1 (Classical.not_not.2 h) (mem_of_max (degree_eq_natDegree hp)),
    fun h => h.symm ▸ leadingCoeff_zero⟩
Leading Coefficient Vanishes if and only if Polynomial is Zero
Informal description
For a polynomial $p \in R[X]$, the leading coefficient of $p$ is zero if and only if $p$ is the zero polynomial. In other words, $\text{leadingCoeff}(p) = 0 \leftrightarrow p = 0$.
Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot theorem
: leadingCoeff p = 0 ↔ degree p = ⊥
Full source 
theorem leadingCoeff_eq_zero_iff_deg_eq_bot : leadingCoeffleadingCoeff p = 0 ↔ degree p = ⊥ := by
  rw [leadingCoeff_eq_zero, degree_eq_bot]
Leading Coefficient Vanishes if and only if Degree is Bottom
Informal description
For a polynomial $p \in R[X]$, the leading coefficient of $p$ is zero if and only if the degree of $p$ is equal to the bottom element $\bot$ (i.e., $p$ is the zero polynomial). In other words, $\text{leadingCoeff}(p) = 0 \leftrightarrow \deg(p) = \bot$.
Polynomial.natDegree_C_mul_X_pow_le theorem
(a : R) (n : ℕ) : natDegree (C a * X ^ n) ≤ n
Full source 
theorem natDegree_C_mul_X_pow_le (a : R) (n : ℕ) : natDegree (C a * X ^ n) ≤ n :=
  natDegree_le_iff_degree_le.2 <| degree_C_mul_X_pow_le _ _
Natural Degree Bound for Monomials: $\operatorname{natDegree}(a X^n) \leq n$
Informal description
For any coefficient $a$ in a semiring $R$ and any natural number $n$, the natural degree of the monomial $a X^n$ is less than or equal to $n$. That is, $\operatorname{natDegree}(a X^n) \leq n$.
Polynomial.degree_erase_le theorem
(p : R[X]) (n : ℕ) : degree (p.erase n) ≤ degree p
Full source 
theorem degree_erase_le (p : R[X]) (n : ℕ) : degree (p.erase n) ≤ degree p := by
  rcases p with ⟨p⟩
  simp only [erase_def, degree, coeff, support]
  apply sup_mono
  rw [Finsupp.support_erase]
  apply Finset.erase_subset
Degree Inequality for Polynomial Term Erasure
Informal description
For any polynomial $p \in R[X]$ and any natural number $n$, the degree of the polynomial obtained by removing the term of degree $n$ from $p$ is less than or equal to the degree of $p$. That is, $\deg(\operatorname{erase}(p, n)) \leq \deg(p)$.
Polynomial.degree_erase_lt theorem
(hp : p ≠ 0) : degree (p.erase (natDegree p)) < degree p
Full source 
theorem degree_erase_lt (hp : p ≠ 0) : degree (p.erase (natDegree p)) < degree p := by
  apply lt_of_le_of_ne (degree_erase_le _ _)
  rw [degree_eq_natDegree hp, degree, support_erase]
  exact fun h => not_mem_erase _ _ (mem_of_max h)
Strict Degree Reduction After Erasing Leading Term: $\deg(\operatorname{erase}(p, \operatorname{natDegree}(p))) < \deg(p)$
Informal description
For any nonzero polynomial $p \in R[X]$, the degree of the polynomial obtained by removing the term of degree $\operatorname{natDegree}(p)$ from $p$ is strictly less than the degree of $p$, i.e., \[ \deg(\operatorname{erase}(p, \operatorname{natDegree}(p))) < \deg(p). \]
Polynomial.degree_update_le theorem
(p : R[X]) (n : ℕ) (a : R) : degree (p.update n a) ≤ max (degree p) n
Full source 
theorem degree_update_le (p : R[X]) (n : ℕ) (a : R) : degree (p.update n a) ≤ max (degree p) n := by
  classical
  rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl
Degree Bound for Polynomial Coefficient Update: $\deg(p.\text{update}(n, a)) \leq \max(\deg(p), n)$
Informal description
For any polynomial $p \in R[X]$, natural number $n$, and element $a \in R$, the degree of the polynomial obtained by updating the coefficient of $X^n$ in $p$ to $a$ satisfies the inequality: \[ \deg(p.\text{update}(n, a)) \leq \max(\deg(p), n). \]
Polynomial.degree_sum_le theorem
(s : Finset ι) (f : ι → R[X]) : degree (∑ i ∈ s, f i) ≤ s.sup fun b => degree (f b)
Full source 
theorem degree_sum_le (s : Finset ι) (f : ι → R[X]) :
    degree (∑ i ∈ s, f i) ≤ s.sup fun b => degree (f b) :=
  Finset.cons_induction_on s (by simp only [sum_empty, sup_empty, degree_zero, le_refl])
    fun a s has ih =>
    calc
      degree (∑ i ∈ cons a s has, f i) ≤ max (degree (f a)) (degree (∑ i ∈ s, f i)) := by
        rw [Finset.sum_cons]; exact degree_add_le _ _
      _ ≤ _ := by rw [sup_cons]; exact max_le_max le_rfl ih
Degree Bound for Sum of Polynomials: $\deg(\sum f_i) \leq \max \deg(f_i)$
Informal description
For any finite set $s$ of indices and any family of polynomials $(f_i)_{i \in s}$ over a semiring $R$, the degree of the sum $\sum_{i \in s} f_i$ is bounded by the maximum degree among the polynomials $f_i$, i.e., \[ \deg\left(\sum_{i \in s} f_i\right) \leq \max_{i \in s} \deg(f_i). \]
Polynomial.degree_mul_le theorem
(p q : R[X]) : degree (p * q) ≤ degree p + degree q
Full source 
theorem degree_mul_le (p q : R[X]) : degree (p * q) ≤ degree p + degree q := by
  simpa only [degree, ← support_toFinsupp, toFinsupp_mul]
    using AddMonoidAlgebra.sup_support_mul_le (WithBot.coe_add _ _).le _ _
Degree Bound for Polynomial Multiplication: $\deg(p \cdot q) \leq \deg(p) + \deg(q)$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, the degree of their product satisfies the inequality: \[ \deg(p \cdot q) \leq \deg(p) + \deg(q). \]
Polynomial.degree_mul_le_of_le theorem
{a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) : degree (p * q) ≤ a + b
Full source 
theorem degree_mul_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) :
    degree (p * q) ≤ a + b :=
  (p.degree_mul_le _).trans <| add_le_add ‹_› ‹_›
Degree Bound for Polynomial Multiplication with Given Degree Constraints: $\deg(p \cdot q) \leq a + b$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, if the degree of $p$ is at most $a$ and the degree of $q$ is at most $b$ (where $a, b \in \mathbb{N} \cup \{\bot\}$), then the degree of their product satisfies: \[ \deg(p \cdot q) \leq a + b. \]
Polynomial.degree_pow_le theorem
(p : R[X]) : ∀ n : ℕ, degree (p ^ n) ≤ n • degree p
Full source 
theorem degree_pow_le (p : R[X]) : ∀ n : ℕ, degree (p ^ n) ≤ n • degree p
  | 0 => by rw [pow_zero, zero_nsmul]; exact degree_one_le
  | n + 1 =>
    calc
      degree (p ^ (n + 1)) ≤ degree (p ^ n) + degree p := by
        rw [pow_succ]; exact degree_mul_le _ _
      _ ≤ _ := by rw [succ_nsmul]; exact add_le_add_right (degree_pow_le _ _) _
Degree Bound for Polynomial Powers: $\deg(p^n) \leq n \cdot \deg(p)$
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any natural number $n$, the degree of the polynomial power $p^n$ satisfies the inequality: \[ \deg(p^n) \leq n \cdot \deg(p). \]
Polynomial.degree_pow_le_of_le theorem
{a : WithBot ℕ} (b : ℕ) (hp : degree p ≤ a) : degree (p ^ b) ≤ b * a
Full source 
theorem degree_pow_le_of_le {a : WithBot ℕ} (b : ℕ) (hp : degree p ≤ a) :
    degree (p ^ b) ≤ b * a := by
  induction b with
  | zero => simp [degree_one_le]
  | succ n hn =>
      rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
      exact degree_mul_le_of_le hn hp
Degree Bound for Polynomial Powers: $\deg(p^b) \leq b \cdot \deg(p)$
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$, if the degree of $p$ is at most $a$ (where $a \in \mathbb{N} \cup \{\bot\}$), then for any natural number $b$, the degree of $p^b$ satisfies: \[ \deg(p^b) \leq b \cdot a. \]
Polynomial.leadingCoeff_monomial theorem
(a : R) (n : ℕ) : leadingCoeff (monomial n a) = a
Full source 
@[simp]
theorem leadingCoeff_monomial (a : R) (n : ℕ) : leadingCoeff (monomial n a) = a := by
  classical
  by_cases ha : a = 0
  · simp only [ha, (monomial n).map_zero, leadingCoeff_zero]
  · rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]
    simp
Leading coefficient of monomial: $\text{lead}(a X^n) = a$
Informal description
For any coefficient $a$ in a semiring $R$ and any natural number $n$, the leading coefficient of the monomial $a X^n$ is equal to $a$.
Polynomial.leadingCoeff_C_mul_X_pow theorem
(a : R) (n : ℕ) : leadingCoeff (C a * X ^ n) = a
Full source 
theorem leadingCoeff_C_mul_X_pow (a : R) (n : ℕ) : leadingCoeff (C a * X ^ n) = a := by
  rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]
Leading coefficient of monomial: $\text{lead}(a X^n) = a$
Informal description
For any coefficient $a$ in a semiring $R$ and any natural number $n$, the leading coefficient of the polynomial $a X^n$ is equal to $a$. That is, \[ \text{lead}(a X^n) = a. \]
Polynomial.leadingCoeff_C_mul_X theorem
(a : R) : leadingCoeff (C a * X) = a
Full source 
theorem leadingCoeff_C_mul_X (a : R) : leadingCoeff (C a * X) = a := by
  simpa only [pow_one] using leadingCoeff_C_mul_X_pow a 1
Leading coefficient of linear monomial: $\text{lead}(a X) = a$
Informal description
For any element $a$ in a semiring $R$, the leading coefficient of the polynomial $a X$ is equal to $a$, i.e., \[ \text{lead}(a X) = a. \]
Polynomial.leadingCoeff_C theorem
(a : R) : leadingCoeff (C a) = a
Full source 
@[simp]
theorem leadingCoeff_C (a : R) : leadingCoeff (C a) = a :=
  leadingCoeff_monomial a 0
Leading coefficient of constant polynomial: $\text{lead}(C(a)) = a$
Informal description
For any element $a$ in a semiring $R$, the leading coefficient of the constant polynomial $C(a)$ is equal to $a$.
Polynomial.leadingCoeff_X_pow theorem
(n : ℕ) : leadingCoeff ((X : R[X]) ^ n) = 1
Full source 
theorem leadingCoeff_X_pow (n : ℕ) : leadingCoeff ((X : R[X]) ^ n) = 1 := by
  simpa only [C_1, one_mul] using leadingCoeff_C_mul_X_pow (1 : R) n
Leading coefficient of $X^n$ is $1$
Informal description
For any natural number $n$, the leading coefficient of the polynomial $X^n$ in the polynomial ring $R[X]$ is equal to $1$.
Polynomial.leadingCoeff_X theorem
: leadingCoeff (X : R[X]) = 1
Full source 
theorem leadingCoeff_X : leadingCoeff (X : R[X]) = 1 := by
  simpa only [pow_one] using @leadingCoeff_X_pow R _ 1
Leading Coefficient of $X$ is $1$
Informal description
The leading coefficient of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to $1$, i.e., $\text{lead}(X) = 1$.
Polynomial.monic_X_pow theorem
(n : ℕ) : Monic (X ^ n : R[X])
Full source 
@[simp]
theorem monic_X_pow (n : ℕ) : Monic (X ^ n : R[X]) :=
  leadingCoeff_X_pow n
Monic Property of $X^n$ in Polynomial Ring $R[X]$
Informal description
For any natural number $n$, the polynomial $X^n$ in the polynomial ring $R[X]$ is monic, i.e., its leading coefficient is equal to $1$.
Polynomial.monic_X theorem
: Monic (X : R[X])
Full source 
@[simp]
theorem monic_X : Monic (X : R[X]) :=
  leadingCoeff_X
Monic Property of $X$ in Polynomial Ring $R[X]$
Informal description
The polynomial variable $X$ in the polynomial ring $R[X]$ is monic, i.e., its leading coefficient is equal to $1$.
Polynomial.leadingCoeff_one theorem
: leadingCoeff (1 : R[X]) = 1
Full source 
theorem leadingCoeff_one : leadingCoeff (1 : R[X]) = 1 :=
  leadingCoeff_C 1
Leading Coefficient of the Unit Polynomial: $\text{lead}(1) = 1$
Informal description
The leading coefficient of the constant polynomial $1$ in the polynomial ring $R[X]$ is equal to $1$.
Polynomial.monic_one theorem
: Monic (1 : R[X])
Full source 
@[simp]
theorem monic_one : Monic (1 : R[X]) :=
  leadingCoeff_C _
Monic Property of the Constant One Polynomial
Informal description
The constant polynomial $1 \in R[X]$ is monic, meaning its leading coefficient is equal to $1$.
Polynomial.Monic.ne_zero theorem
{R : Type*} [Semiring R] [Nontrivial R] {p : R[X]} (hp : p.Monic) : p ≠ 0
Full source 
theorem Monic.ne_zero {R : Type*} [Semiring R] [Nontrivial R] {p : R[X]} (hp : p.Monic) :
    p ≠ 0 := by
  rintro rfl
  simp [Monic] at hp
Monic Polynomials are Nonzero in Nontrivial Semirings
Informal description
Let $R$ be a nontrivial semiring and $p \in R[X]$ a monic polynomial. Then $p$ is not the zero polynomial.
Polynomial.Monic.ne_zero_of_ne theorem
(h : (0 : R) ≠ 1) {p : R[X]} (hp : p.Monic) : p ≠ 0
Full source 
theorem Monic.ne_zero_of_ne (h : (0 : R) ≠ 1) {p : R[X]} (hp : p.Monic) : p ≠ 0 := by
  nontriviality R
  exact hp.ne_zero
Nonzero Property of Monic Polynomials in Semirings with Distinct Zero and One
Informal description
Let $R$ be a semiring where $0 \neq 1$, and let $p \in R[X]$ be a monic polynomial. Then $p$ is not the zero polynomial.
Polynomial.Monic.ne_zero_of_polynomial_ne theorem
{r} (hp : Monic p) (hne : q ≠ r) : p ≠ 0
Full source 
theorem Monic.ne_zero_of_polynomial_ne {r} (hp : Monic p) (hne : q ≠ r) : p ≠ 0 :=
  haveI := Nontrivial.of_polynomial_ne hne
  hp.ne_zero
Nonzero Property of Monic Polynomials under Polynomial Inequality
Informal description
Let $R$ be a semiring and let $p, q, r \in R[X]$ be polynomials. If $p$ is monic and $q \neq r$, then $p$ is not the zero polynomial.
Polynomial.natDegree_mul_le theorem
{p q : R[X]} : natDegree (p * q) ≤ natDegree p + natDegree q
Full source 
theorem natDegree_mul_le {p q : R[X]} : natDegree (p * q) ≤ natDegree p + natDegree q := by
  apply natDegree_le_of_degree_le
  apply le_trans (degree_mul_le p q)
  rw [Nat.cast_add]
  apply add_le_add <;> apply degree_le_natDegree
Natural Degree Bound for Polynomial Multiplication: $\text{natDegree}(p \cdot q) \leq \text{natDegree}(p) + \text{natDegree}(q)$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, the natural degree of their product satisfies the inequality: \[ \text{natDegree}(p \cdot q) \leq \text{natDegree}(p) + \text{natDegree}(q). \]
Polynomial.natDegree_mul_le_of_le theorem
(hp : natDegree p ≤ m) (hg : natDegree q ≤ n) : natDegree (p * q) ≤ m + n
Full source 
theorem natDegree_mul_le_of_le (hp : natDegree p ≤ m) (hg : natDegree q ≤ n) :
    natDegree (p * q) ≤ m + n :=
natDegree_mul_le.trans <| add_le_add ‹_› ‹_›
Degree Bound for Polynomial Multiplication: $\text{natDegree}(p \cdot q) \leq m + n$ when $\text{natDegree}(p) \leq m$ and $\text{natDegree}(q) \leq n$
Informal description
For any two polynomials $p, q \in R[X]$ over a semiring $R$, if the natural degree of $p$ is at most $m$ and the natural degree of $q$ is at most $n$, then the natural degree of their product satisfies: \[ \text{natDegree}(p \cdot q) \leq m + n. \]
Polynomial.natDegree_pow_le theorem
{p : R[X]} {n : ℕ} : (p ^ n).natDegree ≤ n * p.natDegree
Full source 
theorem natDegree_pow_le {p : R[X]} {n : ℕ} : (p ^ n).natDegree ≤ n * p.natDegree := by
  induction n with
  | zero => simp
  | succ i hi =>
    rw [pow_succ, Nat.succ_mul]
    apply le_trans natDegree_mul_le (add_le_add_right hi _)
Degree Bound for Polynomial Powers: $\text{natDegree}(p^n) \leq n \cdot \text{natDegree}(p)$
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any natural number $n$, the natural degree of $p^n$ satisfies the inequality: \[ \text{natDegree}(p^n) \leq n \cdot \text{natDegree}(p). \]
Polynomial.natDegree_pow_le_of_le theorem
(n : ℕ) (hp : natDegree p ≤ m) : natDegree (p ^ n) ≤ n * m
Full source 
theorem natDegree_pow_le_of_le (n : ℕ) (hp : natDegree p ≤ m) :
    natDegree (p ^ n) ≤ n * m :=
  natDegree_pow_le.trans (Nat.mul_le_mul le_rfl ‹_›)
Degree Bound for Polynomial Powers with Given Degree Constraint: $\text{natDegree}(p^n) \leq n \cdot m$ when $\text{natDegree}(p) \leq m$
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any natural number $n$, if the natural degree of $p$ is at most $m$, then the natural degree of $p^n$ satisfies: \[ \text{natDegree}(p^n) \leq n \cdot m. \]
Polynomial.natDegree_eq_zero_iff_degree_le_zero theorem
: p.natDegree = 0 ↔ p.degree ≤ 0
Full source 
theorem natDegree_eq_zero_iff_degree_le_zero : p.natDegree = 0 ↔ p.degree ≤ 0 := by
  rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]
Natural Degree Zero iff Degree at Most Zero
Informal description
For a polynomial $p \in R[X]$, the natural degree of $p$ is zero if and only if the degree of $p$ (as an element of $\mathbb{N} \cup \{\bot\}$) is less than or equal to zero.
Polynomial.degree_zero_le theorem
: degree (0 : R[X]) ≤ 0
Full source 
theorem degree_zero_le : degree (0 : R[X]) ≤ 0 := natDegree_eq_zero_iff_degree_le_zero.mp rfl
Degree of Zero Polynomial is at Most Zero
Informal description
For the zero polynomial $0 \in R[X]$, its degree is less than or equal to $0$ (where degree is considered in $\mathbb{N} \cup \{\bot\}$).
Polynomial.degree_le_iff_coeff_zero theorem
(f : R[X]) (n : WithBot ℕ) : degree f ≤ n ↔ ∀ m : ℕ, n < m → coeff f m = 0
Full source 
theorem degree_le_iff_coeff_zero (f : R[X]) (n : WithBot ℕ) :
    degreedegree f ≤ n ↔ ∀ m : ℕ, n < m → coeff f m = 0 := by
  simp only [degree, Finset.max, Finset.sup_le_iff, mem_support_iff, Ne, ← not_le,
    not_imp_comm, Nat.cast_withBot]
Characterization of Polynomial Degree via Vanishing Coefficients
Informal description
For a polynomial $f \in R[X]$ and a natural number $n$ (or $\bot$), the degree of $f$ is less than or equal to $n$ if and only if all coefficients of $f$ corresponding to exponents greater than $n$ are zero. More precisely, $\deg(f) \leq n$ if and only if for every natural number $m > n$, the coefficient of $X^m$ in $f$ is zero.
Polynomial.degree_lt_iff_coeff_zero theorem
(f : R[X]) (n : ℕ) : degree f < n ↔ ∀ m : ℕ, n ≤ m → coeff f m = 0
Full source 
theorem degree_lt_iff_coeff_zero (f : R[X]) (n : ℕ) :
    degreedegree f < n ↔ ∀ m : ℕ, n ≤ m → coeff f m = 0 := by
  simp only [degree, Finset.sup_lt_iff (WithBot.bot_lt_coe n), mem_support_iff,
    WithBot.coe_lt_coe, ← @not_le ℕ, max_eq_sup_coe, Nat.cast_withBot, Ne, not_imp_not]
Characterization of Polynomial Degree Strictly Less Than $n$ via Vanishing Coefficients
Informal description
For a polynomial $f \in R[X]$ and a natural number $n$, the degree of $f$ is strictly less than $n$ if and only if all coefficients of $f$ corresponding to exponents greater than or equal to $n$ are zero. That is, \[ \deg(f) < n \leftrightarrow \forall m \geq n, \text{coeff}(f, m) = 0. \]
Polynomial.degree_X_pow theorem
: degree ((X : R[X]) ^ n) = n
Full source 
@[simp]
theorem degree_X_pow : degree ((X : R[X]) ^ n) = n := by
  rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]
Degree of $X^n$ is $n$
Informal description
For any natural number $n$, the degree of the polynomial $X^n$ in the polynomial ring $R[X]$ is equal to $n$.
Polynomial.natDegree_X_pow theorem
: natDegree ((X : R[X]) ^ n) = n
Full source 
@[simp]
theorem natDegree_X_pow : natDegree ((X : R[X]) ^ n) = n :=
  natDegree_eq_of_degree_eq_some (degree_X_pow n)
Natural Degree of $X^n$ is $n$
Informal description
For any natural number $n$, the natural degree of the polynomial $X^n$ in the polynomial ring $R[X]$ is equal to $n$.
Polynomial.degree_sub_le theorem
(p q : R[X]) : degree (p - q) ≤ max (degree p) (degree q)
Full source 
theorem degree_sub_le (p q : R[X]) : degree (p - q) ≤ max (degree p) (degree q) := by
  simpa only [degree_neg q] using degree_add_le p (-q)
Degree Bound for Difference of Polynomials: $\deg(p - q) \leq \max(\deg p, \deg q)$
Informal description
For any two polynomials $p, q \in R[X]$ over a ring $R$, the degree of their difference satisfies $\deg(p - q) \leq \max(\deg p, \deg q)$, where $\deg$ denotes the polynomial degree (with $\deg 0 = \bot$).
Polynomial.degree_sub_le_of_le theorem
{a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) : degree (p - q) ≤ max a b
Full source 
theorem degree_sub_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) :
    degree (p - q) ≤ max a b :=
  (p.degree_sub_le q).trans <| max_le_max ‹_› ‹_›
Degree Bound for Difference of Polynomials with Given Bounds: $\deg(p - q) \leq \max(a, b)$
Informal description
For any two polynomials $p, q \in R[X]$ over a ring $R$, if the degree of $p$ is bounded above by $a \in \mathbb{N} \cup \{\bot\}$ and the degree of $q$ is bounded above by $b \in \mathbb{N} \cup \{\bot\}$, then the degree of their difference $p - q$ satisfies $\deg(p - q) \leq \max(a, b)$.
Polynomial.natDegree_sub_le theorem
(p q : R[X]) : natDegree (p - q) ≤ max (natDegree p) (natDegree q)
Full source 
theorem natDegree_sub_le (p q : R[X]) : natDegree (p - q) ≤ max (natDegree p) (natDegree q) := by
  simpa only [← natDegree_neg q] using natDegree_add_le p (-q)
Natural Degree Bound for Difference of Polynomials: $\mathrm{natDegree}(p - q) \leq \max(\mathrm{natDegree}(p), \mathrm{natDegree}(q))$
Informal description
For any two polynomials $p, q \in R[X]$ over a ring $R$, the natural degree of their difference satisfies $\mathrm{natDegree}(p - q) \leq \max(\mathrm{natDegree}(p), \mathrm{natDegree}(q))$.
Polynomial.natDegree_sub_le_of_le theorem
(hp : natDegree p ≤ m) (hq : natDegree q ≤ n) : natDegree (p - q) ≤ max m n
Full source 
theorem natDegree_sub_le_of_le (hp : natDegree p ≤ m) (hq : natDegree q ≤ n) :
    natDegree (p - q) ≤ max m n :=
  (p.natDegree_sub_le q).trans <| max_le_max ‹_› ‹_›
Natural Degree Bound for Difference of Bounded Polynomials: $\mathrm{natDegree}(p - q) \leq \max(m, n)$
Informal description
For any two polynomials $p, q \in R[X]$ over a ring $R$, if the natural degree of $p$ is at most $m$ and the natural degree of $q$ is at most $n$, then the natural degree of their difference satisfies $\mathrm{natDegree}(p - q) \leq \max(m, n)$.
Polynomial.degree_sub_lt theorem
(hd : degree p = degree q) (hp0 : p ≠ 0) (hlc : leadingCoeff p = leadingCoeff q) : degree (p - q) < degree p
Full source 
theorem degree_sub_lt (hd : degree p = degree q) (hp0 : p ≠ 0)
    (hlc : leadingCoeff p = leadingCoeff q) : degree (p - q) < degree p :=
  have hp : monomial (natDegree p) (leadingCoeff p) + p.erase (natDegree p) = p :=
    monomial_add_erase _ _
  have hq : monomial (natDegree q) (leadingCoeff q) + q.erase (natDegree q) = q :=
    monomial_add_erase _ _
  have hd' : natDegree p = natDegree q := by unfold natDegree; rw [hd]
  have hq0 : q ≠ 0 := mt degree_eq_bot.2 (hd ▸ mt degree_eq_bot.1 hp0)
  calc
    degree (p - q) = degree (erase (natDegree q) p + -erase (natDegree q) q) := by
      conv =>
        lhs
        rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]
    _ ≤ max (degree (erase (natDegree q) p)) (degree (erase (natDegree q) q)) :=
      (degree_neg (erase (natDegree q) q) ▸ degree_add_le _ _)
    _ < degree p := max_lt_iff.2 ⟨hd' ▸ degree_erase_lt hp0, hd.symm ▸ degree_erase_lt hq0⟩
Degree Reduction in Polynomial Subtraction: $\deg(p - q) < \deg(p)$ under equal degrees and leading coefficients
Informal description
For any two nonzero polynomials $p, q \in R[X]$ over a ring $R$ with equal degrees and equal leading coefficients, the degree of their difference $p - q$ is strictly less than the degree of $p$. That is, if $\deg(p) = \deg(q)$, $p \neq 0$, and $\text{lc}(p) = \text{lc}(q)$, then $\deg(p - q) < \deg(p)$.
Polynomial.natDegree_X_sub_C_le theorem
(r : R) : (X - C r).natDegree ≤ 1
Full source 
theorem natDegree_X_sub_C_le (r : R) : (X - C r).natDegree ≤ 1 :=
  natDegree_le_iff_degree_le.2 <| degree_X_sub_C_le r
Natural Degree Bound for Linear Polynomial: $\text{natDegree}(X - r) \leq 1$
Informal description
For any element $r$ in a ring $R$, the natural degree of the polynomial $X - r$ in $R[X]$ is less than or equal to $1$.