Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Polynomial.trailingDegree definition

(p : R[X]) : ℕ∞

Full source

/-- `trailingDegree p` is the multiplicity of `x` in the polynomial `p`, i.e. the smallest
`X`-exponent in `p`.
`trailingDegree p = some n` when `p ≠ 0` and `n` is the smallest power of `X` that appears
in `p`, otherwise
`trailingDegree 0 = ⊤`. -/
def trailingDegree (p : R[X]) : ℕ∞ :=
  p.support.min

Trailing degree of a polynomial

Informal description

For a polynomial $ p \in R[X] $, the trailing degree $\text{trailingDegree}(p)$ is defined as the smallest exponent $ n $ such that the coefficient of $ X^n $ in $ p $ is nonzero. If $ p = 0 $, then $\text{trailingDegree}(p) = \infty$. More formally, $\text{trailingDegree}(p)$ is the minimum element of the support of $ p $ (the set of exponents with nonzero coefficients), viewed as an element of the extended natural numbers $\mathbb{N}_\infty$.

Polynomial.trailingDegree_lt_wf theorem

: WellFounded fun p q : R[X] => trailingDegree p < trailingDegree q

Full source

theorem trailingDegree_lt_wf : WellFounded fun p q : R[X] => trailingDegree p < trailingDegree q :=
  InvImage.wf trailingDegree wellFounded_lt

Well-foundedness of the trailing degree relation on polynomials

Informal description

The relation on polynomials $p, q \in R[X]$ defined by $\text{trailingDegree}(p) < \text{trailingDegree}(q)$ is well-founded.

Polynomial.natTrailingDegree definition

(p : R[X]) : ℕ

Full source

/-- `natTrailingDegree p` forces `trailingDegree p` to `ℕ`, by defining
`natTrailingDegree ⊤ = 0`. -/
def natTrailingDegree (p : R[X]) : ℕ :=
  ENat.toNat (trailingDegree p)

Natural trailing degree of a polynomial

Informal description

For a polynomial $ p \in R[X] $, the natural trailing degree $\text{natTrailingDegree}(p)$ is defined as the smallest exponent $ n $ such that the coefficient of $ X^n $ in $ p $ is nonzero, converted to a natural number (with $\infty$ mapped to $0$).

Polynomial.trailingCoeff definition

(p : R[X]) : R

Full source

/-- `trailingCoeff p` gives the coefficient of the smallest power of `X` in `p`. -/
def trailingCoeff (p : R[X]) : R :=
  coeff p (natTrailingDegree p)

Trailing coefficient of a polynomial

Informal description

For a polynomial $ p \in R[X] $, the trailing coefficient $\text{trailingCoeff}(p)$ is the coefficient of the term $X^{\text{natTrailingDegree}(p)}$ in $p$, where $\text{natTrailingDegree}(p)$ is the smallest exponent $n$ such that the coefficient of $X^n$ in $p$ is nonzero.

Polynomial.TrailingMonic definition

(p : R[X])

Full source

/-- a polynomial is `monic_at` if its trailing coefficient is 1 -/
def TrailingMonic (p : R[X]) :=
  trailingCoeff p = (1 : R)

Trailing monic polynomial

Informal description

A polynomial $ p \in R[X] $ is called *trailing monic* if its trailing coefficient (the coefficient of the term with smallest degree) is equal to 1.

Polynomial.TrailingMonic.def theorem

: TrailingMonic p ↔ trailingCoeff p = 1

Full source

theorem TrailingMonic.def : TrailingMonicTrailingMonic p ↔ trailingCoeff p = 1 :=
  Iff.rfl

Characterization of Trailing Monic Polynomials: $\text{trailingCoeff}(p) = 1$

Informal description

A polynomial $p \in R[X]$ is trailing monic if and only if its trailing coefficient equals $1$, i.e., $\text{trailingCoeff}(p) = 1$.

Polynomial.TrailingMonic.decidable instance

[DecidableEq R] : Decidable (TrailingMonic p)

Full source

instance TrailingMonic.decidable [DecidableEq R] : Decidable (TrailingMonic p) :=
  inferInstanceAs <| Decidable (trailingCoeff p = (1 : R))

Decidability of Trailing Monic Polynomials

Informal description

For any polynomial $ p \in R[X] $ over a semiring $ R $ with decidable equality, it is decidable whether $ p $ is trailing monic (i.e., whether its trailing coefficient is equal to 1).

Polynomial.TrailingMonic.trailingCoeff theorem

{p : R[X]} (hp : p.TrailingMonic) : trailingCoeff p = 1

Full source

@[simp]
theorem TrailingMonic.trailingCoeff {p : R[X]} (hp : p.TrailingMonic) : trailingCoeff p = 1 :=
  hp

Trailing coefficient of a trailing monic polynomial is 1

Informal description

For any polynomial $p \in R[X]$ that is trailing monic, the trailing coefficient of $p$ is equal to $1$.

Polynomial.trailingDegree_zero theorem

: trailingDegree (0 : R[X]) = ⊤

Full source

@[simp]
theorem trailingDegree_zero : trailingDegree (0 : R[X]) = ⊤ :=
  rfl

Trailing degree of the zero polynomial is infinity

Informal description

For the zero polynomial $0 \in R[X]$, the trailing degree is $\infty$, i.e., $\text{trailingDegree}(0) = \infty$.

Polynomial.trailingCoeff_zero theorem

: trailingCoeff (0 : R[X]) = 0

Full source

@[simp]
theorem trailingCoeff_zero : trailingCoeff (0 : R[X]) = 0 :=
  rfl

Trailing Coefficient of Zero Polynomial is Zero

Informal description

The trailing coefficient of the zero polynomial $0 \in R[X]$ is equal to $0$.

Polynomial.natTrailingDegree_zero theorem

: natTrailingDegree (0 : R[X]) = 0

Full source

@[simp]
theorem natTrailingDegree_zero : natTrailingDegree (0 : R[X]) = 0 :=
  rfl

Natural trailing degree of the zero polynomial is zero

Informal description

For the zero polynomial $0 \in R[X]$, the natural trailing degree is $0$, i.e., $\text{natTrailingDegree}(0) = 0$.

Polynomial.trailingDegree_eq_top theorem

: trailingDegree p = ⊤ ↔ p = 0

Full source

@[simp]
theorem trailingDegree_eq_top : trailingDegreetrailingDegree p = ⊤ ↔ p = 0 :=
  ⟨fun h => support_eq_empty.1 (Finset.min_eq_top.1 h), fun h => by simp [h]⟩

Trailing Degree is Infinite if and only if Polynomial is Zero

Informal description

For a polynomial $p \in R[X]$, the trailing degree of $p$ is equal to $\infty$ if and only if $p$ is the zero polynomial. That is, $\text{trailingDegree}(p) = \infty \leftrightarrow p = 0$.

Polynomial.trailingDegree_eq_natTrailingDegree theorem

(hp : p ≠ 0) : trailingDegree p = (natTrailingDegree p : ℕ∞)

Full source

theorem trailingDegree_eq_natTrailingDegree (hp : p ≠ 0) :
    trailingDegree p = (natTrailingDegree p : ℕ∞) :=
  .symm <| ENat.coe_toNat <| mt trailingDegree_eq_top.1 hp

Trailing Degree Equals Natural Trailing Degree for Nonzero Polynomials

Informal description

For any nonzero polynomial $p \in R[X]$, the trailing degree of $p$ is equal to its natural trailing degree when viewed as an extended natural number. That is, $\text{trailingDegree}(p) = \text{natTrailingDegree}(p)$.

Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq theorem

{p : R[X]} {n : ℕ} (hp : p ≠ 0) : p.trailingDegree = n ↔ p.natTrailingDegree = n

Full source

theorem trailingDegree_eq_iff_natTrailingDegree_eq {p : R[X]} {n : ℕ} (hp : p ≠ 0) :
    p.trailingDegree = n ↔ p.natTrailingDegree = n := by
  rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]

Equivalence of Trailing Degree and Natural Trailing Degree for Nonzero Polynomials

Informal description

For any nonzero polynomial $p \in R[X]$ and natural number $n$, the trailing degree of $p$ equals $n$ if and only if the natural trailing degree of $p$ equals $n$. That is, $\text{trailingDegree}(p) = n \leftrightarrow \text{natTrailingDegree}(p) = n$.

Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq_of_pos theorem

{p : R[X]} {n : ℕ} (hn : n ≠ 0) : p.trailingDegree = n ↔ p.natTrailingDegree = n

Full source

theorem trailingDegree_eq_iff_natTrailingDegree_eq_of_pos {p : R[X]} {n : ℕ} (hn : n ≠ 0) :
    p.trailingDegree = n ↔ p.natTrailingDegree = n := by
  rw [natTrailingDegree, ENat.toNat_eq_iff hn]

Equivalence of Trailing Degree and Natural Trailing Degree for Nonzero Polynomials and Nonzero Degrees

Informal description

For a nonzero polynomial $p \in R[X]$ and a nonzero natural number $n \in \mathbb{N}$, the trailing degree of $p$ equals $n$ if and only if the natural trailing degree of $p$ equals $n$. That is, $\text{trailingDegree}(p) = n \leftrightarrow \text{natTrailingDegree}(p) = n$.

Polynomial.natTrailingDegree_eq_of_trailingDegree_eq_some theorem

{p : R[X]} {n : ℕ} (h : trailingDegree p = n) : natTrailingDegree p = n

Full source

theorem natTrailingDegree_eq_of_trailingDegree_eq_some {p : R[X]} {n : ℕ}
    (h : trailingDegree p = n) : natTrailingDegree p = n := by
  simp [natTrailingDegree, h]

Equality of Natural Trailing Degree Given Trailing Degree

Informal description

For any nonzero polynomial $p \in R[X]$ and natural number $n$, if the trailing degree of $p$ is equal to $n$ (i.e., $\text{trailingDegree}(p) = n$), then the natural trailing degree of $p$ is also equal to $n$ (i.e., $\text{natTrailingDegree}(p) = n$).

Polynomial.natTrailingDegree_le_trailingDegree theorem

: ↑(natTrailingDegree p) ≤ trailingDegree p

Full source

@[simp]
theorem natTrailingDegree_le_trailingDegree : ↑(natTrailingDegree p) ≤ trailingDegree p :=
  ENat.coe_toNat_le_self _

Natural Trailing Degree Bounded by Trailing Degree in Polynomials

Informal description

For any univariate polynomial $p$ over a semiring $R$, the natural trailing degree of $p$ (as a natural number) is less than or equal to its trailing degree (as an extended natural number). In other words, if we denote $\text{natTrailingDegree}(p)$ as $n$ and $\text{trailingDegree}(p)$ as $d$, then $n \leq d$ holds in $\mathbb{N}_\infty$.

Polynomial.natTrailingDegree_eq_of_trailingDegree_eq theorem

[Semiring S] {q : S[X]} (h : trailingDegree p = trailingDegree q) : natTrailingDegree p = natTrailingDegree q

Full source

theorem natTrailingDegree_eq_of_trailingDegree_eq [Semiring S] {q : S[X]}
    (h : trailingDegree p = trailingDegree q) : natTrailingDegree p = natTrailingDegree q := by
  unfold natTrailingDegree
  rw [h]

Equality of Natural Trailing Degrees from Equality of Trailing Degrees

Informal description

For polynomials $p \in R[X]$ and $q \in S[X]$ over semirings $R$ and $S$, if the trailing degrees of $p$ and $q$ are equal (i.e., $\text{trailingDegree}(p) = \text{trailingDegree}(q)$), then their natural trailing degrees are also equal (i.e., $\text{natTrailingDegree}(p) = \text{natTrailingDegree}(q)$).

Polynomial.trailingDegree_le_of_ne_zero theorem

(h : coeff p n ≠ 0) : trailingDegree p ≤ n

Full source

theorem trailingDegree_le_of_ne_zero (h : coeffcoeff p n ≠ 0) : trailingDegree p ≤ n :=
  min_le (mem_support_iff.2 h)

Trailing Degree Bound for Nonzero Coefficients: $\text{trailingDegree}(p) \leq n$ when $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 (i.e., $p_n \neq 0$), then the trailing degree of $p$ is less than or equal to $n$ (i.e., $\text{trailingDegree}(p) \leq n$).

Polynomial.natTrailingDegree_le_of_ne_zero theorem

(h : coeff p n ≠ 0) : natTrailingDegree p ≤ n

Full source

theorem natTrailingDegree_le_of_ne_zero (h : coeffcoeff p n ≠ 0) : natTrailingDegree p ≤ n :=
  ENat.toNat_le_of_le_coe <| trailingDegree_le_of_ne_zero h

Natural Trailing Degree Bound for Nonzero Coefficients: $\text{natTrailingDegree}(p) \leq n$ when $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 (i.e., $p_n \neq 0$), then the natural trailing degree of $p$ is less than or equal to $n$ (i.e., $\text{natTrailingDegree}(p) \leq n$).

Polynomial.coeff_natTrailingDegree_eq_zero theorem

: coeff p p.natTrailingDegree = 0 ↔ p = 0

Full source

@[simp] lemma coeff_natTrailingDegree_eq_zero : coeffcoeff p p.natTrailingDegree = 0 ↔ p = 0 := by
  constructor
  · rintro h
    by_contra hp
    obtain ⟨n, hpn, hn⟩ := by simpa using min_mem_image_coe <| support_nonempty.2 hp
    obtain rfl := (trailingDegree_eq_iff_natTrailingDegree_eq hp).1 hn.symm
    exact hpn h
  · rintro rfl
    simp

Zero Coefficient at Natural Trailing Degree Characterizes Zero Polynomial

Informal description

For a polynomial $p \in R[X]$, the coefficient of the term with exponent equal to the natural trailing degree of $p$ is zero if and only if $p$ is the zero polynomial. In other words: \[ p_{\text{natTrailingDegree}(p)} = 0 \leftrightarrow p = 0. \]

Polynomial.coeff_natTrailingDegree_ne_zero theorem

: coeff p p.natTrailingDegree ≠ 0 ↔ p ≠ 0

Full source

lemma coeff_natTrailingDegree_ne_zero : coeffcoeff p p.natTrailingDegree ≠ 0coeff p p.natTrailingDegree ≠ 0 ↔ p ≠ 0 :=
  coeff_natTrailingDegree_eq_zero.not

Nonzero Coefficient at Natural Trailing Degree Characterizes Nonzero Polynomial

Informal description

For a polynomial $p \in R[X]$, the coefficient of the term with exponent equal to the natural trailing degree of $p$ is nonzero if and only if $p$ is not the zero polynomial. In other words: \[ p_{\text{natTrailingDegree}(p)} \neq 0 \leftrightarrow p \neq 0. \]

Polynomial.trailingDegree_eq_zero theorem

: trailingDegree p = 0 ↔ coeff p 0 ≠ 0

Full source

@[simp]
lemma trailingDegree_eq_zero : trailingDegreetrailingDegree p = 0 ↔ coeff p 0 ≠ 0 :=
  Finset.min_eq_bot.trans mem_support_iff

Trailing Degree Zero Characterization: $\text{trailingDegree}(p) = 0 \leftrightarrow p_0 \neq 0$

Informal description

For a polynomial $p \in R[X]$, the trailing degree $\text{trailingDegree}(p)$ is equal to $0$ if and only if the constant term (coefficient of $X^0$) of $p$ is nonzero. In other words: \[ \text{trailingDegree}(p) = 0 \leftrightarrow p_0 \neq 0, \] where $p_0$ denotes the coefficient of $X^0$ in $p$.

Polynomial.natTrailingDegree_eq_zero theorem

: natTrailingDegree p = 0 ↔ p = 0 ∨ coeff p 0 ≠ 0

Full source

@[simp] lemma natTrailingDegree_eq_zero : natTrailingDegreenatTrailingDegree p = 0 ↔ p = 0 ∨ coeff p 0 ≠ 0 := by
  simp [natTrailingDegree, or_comm]

Natural Trailing Degree Equals Zero if and only if Polynomial is Zero or Has Nonzero Constant Term

Informal description

For a polynomial $p \in R[X]$, the natural trailing degree $\text{natTrailingDegree}(p)$ is equal to $0$ if and only if either $p$ is the zero polynomial or the constant term (coefficient of $X^0$) of $p$ is nonzero. In other words: \[ \text{natTrailingDegree}(p) = 0 \leftrightarrow p = 0 \lor p_0 \neq 0, \] where $p_0$ denotes the coefficient of $X^0$ in $p$.

Polynomial.natTrailingDegree_ne_zero theorem

: natTrailingDegree p ≠ 0 ↔ p ≠ 0 ∧ coeff p 0 = 0

Full source

lemma natTrailingDegree_ne_zero : natTrailingDegreenatTrailingDegree p ≠ 0natTrailingDegree p ≠ 0 ↔ p ≠ 0 ∧ coeff p 0 = 0 :=
  natTrailingDegree_eq_zero.not.trans <| by rw [not_or, not_ne_iff]

Nonzero Natural Trailing Degree Characterization for Polynomials

Informal description

For a polynomial $p \in R[X]$, the natural trailing degree $\text{natTrailingDegree}(p)$ is not equal to $0$ if and only if $p$ is not the zero polynomial and its constant term (the coefficient of $X^0$) is zero. In other words: \[ \text{natTrailingDegree}(p) \neq 0 \leftrightarrow p \neq 0 \land p_0 = 0, \] where $p_0$ denotes the coefficient of $X^0$ in $p$.

Polynomial.trailingDegree_ne_zero theorem

: trailingDegree p ≠ 0 ↔ coeff p 0 = 0

Full source

lemma trailingDegree_ne_zero : trailingDegreetrailingDegree p ≠ 0trailingDegree p ≠ 0 ↔ coeff p 0 = 0 :=
  trailingDegree_eq_zero.not_left

Nonzero Trailing Degree Characterization: $\text{trailingDegree}(p) \neq 0 \leftrightarrow p_0 = 0$

Informal description

For a polynomial $p \in R[X]$, the trailing degree $\text{trailingDegree}(p)$ is not equal to $0$ if and only if the constant term (coefficient of $X^0$) of $p$ is zero. In other words: \[ \text{trailingDegree}(p) \neq 0 \leftrightarrow p_0 = 0, \] where $p_0$ denotes the coefficient of $X^0$ in $p$.

Polynomial.trailingDegree_le_trailingDegree theorem

(h : coeff q (natTrailingDegree p) ≠ 0) : trailingDegree q ≤ trailingDegree p

Full source

@[simp] theorem trailingDegree_le_trailingDegree (h : coeffcoeff q (natTrailingDegree p) ≠ 0) :
    trailingDegree q ≤ trailingDegree p :=
  (trailingDegree_le_of_ne_zero h).trans natTrailingDegree_le_trailingDegree

Trailing Degree Comparison for Polynomials with Nonzero Coefficients

Informal description

For polynomials $p$ and $q$ over a semiring $R$, if the coefficient of $X^{\text{natTrailingDegree}(p)}$ in $q$ is nonzero, then the trailing degree of $q$ is less than or equal to the trailing degree of $p$. In other words, if $q_{\text{natTrailingDegree}(p)} \neq 0$, then $\text{trailingDegree}(q) \leq \text{trailingDegree}(p)$.

Polynomial.trailingDegree_ne_of_natTrailingDegree_ne theorem

{n : ℕ} : p.natTrailingDegree ≠ n → trailingDegree p ≠ n

Full source

theorem trailingDegree_ne_of_natTrailingDegree_ne {n : ℕ} :
    p.natTrailingDegree ≠ n → trailingDegreetrailingDegree p ≠ n :=
  mt fun h => by rw [natTrailingDegree, h, ENat.toNat_coe]

Non-equality of trailing degree and natural trailing degree

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, if the natural trailing degree of $p$ is not equal to $n$, then the trailing degree of $p$ (as an extended natural number) is also not equal to $n$.

Polynomial.natTrailingDegree_le_of_trailingDegree_le theorem

{n : ℕ} {hp : p ≠ 0} (H : (n : ℕ∞) ≤ trailingDegree p) : n ≤ natTrailingDegree p

Full source

theorem natTrailingDegree_le_of_trailingDegree_le {n : ℕ} {hp : p ≠ 0}
    (H : (n : ℕ∞) ≤ trailingDegree p) : n ≤ natTrailingDegree p := by
  rwa [trailingDegree_eq_natTrailingDegree hp, Nat.cast_le] at H

Natural Trailing Degree Lower Bound from Trailing Degree Inequality

Informal description

For any polynomial $p \neq 0$ over a semiring $R$ and any natural number $n$, if $n \leq \text{trailingDegree}(p)$ (where $n$ is viewed as an extended natural number), then $n \leq \text{natTrailingDegree}(p)$.

Polynomial.natTrailingDegree_le_natTrailingDegree theorem

(hq : q ≠ 0) (hpq : p.trailingDegree ≤ q.trailingDegree) : p.natTrailingDegree ≤ q.natTrailingDegree

Full source

theorem natTrailingDegree_le_natTrailingDegree (hq : q ≠ 0)
    (hpq : p.trailingDegree ≤ q.trailingDegree) : p.natTrailingDegree ≤ q.natTrailingDegree :=
  ENat.toNat_le_toNat hpq <| by simpa

Natural Trailing Degree Preserves Order for Nonzero Polynomials

Informal description

For any nonzero polynomials $p, q \in R[X]$, if the trailing degree of $p$ is less than or equal to that of $q$, then the natural trailing degree of $p$ is also less than or equal to that of $q$. In other words, if $\text{trailingDegree}(p) \leq \text{trailingDegree}(q)$, then $\text{natTrailingDegree}(p) \leq \text{natTrailingDegree}(q)$.

Polynomial.trailingDegree_monomial theorem

(ha : a ≠ 0) : trailingDegree (monomial n a) = n

Full source

@[simp]
theorem trailingDegree_monomial (ha : a ≠ 0) : trailingDegree (monomial n a) = n := by
  rw [trailingDegree, support_monomial n ha, min_singleton]
  rfl

Trailing Degree of Monomial: $\text{trailingDegree}(a X^n) = n$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$ and any natural number $n$, the trailing degree of the monomial $a X^n$ is equal to $n$.

Polynomial.natTrailingDegree_monomial theorem

(ha : a ≠ 0) : natTrailingDegree (monomial n a) = n

Full source

theorem natTrailingDegree_monomial (ha : a ≠ 0) : natTrailingDegree (monomial n a) = n := by
  rw [natTrailingDegree, trailingDegree_monomial ha]
  rfl

Natural Trailing Degree of Monomial: $\text{natTrailingDegree}(aX^n) = n$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$ and any natural number $n$, the natural trailing degree of the monomial $aX^n$ is equal to $n$.

Polynomial.natTrailingDegree_monomial_le theorem

: natTrailingDegree (monomial n a) ≤ n

Full source

theorem natTrailingDegree_monomial_le : natTrailingDegree (monomial n a) ≤ n :=
  letI := Classical.decEq R
  if ha : a = 0 then by simp [ha] else (natTrailingDegree_monomial ha).le

Upper Bound on Natural Trailing Degree of Monomial: $\text{natTrailingDegree}(aX^n) \leq n$

Informal description

For any natural number $n$ and any element $a$ in a semiring $R$, the natural trailing degree of the monomial $aX^n$ is less than or equal to $n$.

Polynomial.le_trailingDegree_monomial theorem

: ↑n ≤ trailingDegree (monomial n a)

Full source

theorem le_trailingDegree_monomial : ↑n ≤ trailingDegree (monomial n a) :=
  letI := Classical.decEq R
  if ha : a = 0 then by simp [ha] else (trailingDegree_monomial ha).ge

Lower Bound on Trailing Degree of Monomial: $\text{trailingDegree}(a X^n) \geq n$

Informal description

For any natural number $n$ and any element $a$ in a semiring $R$, the trailing degree of the monomial $a X^n$ is greater than or equal to $n$ (when viewed in the extended natural numbers $\mathbb{N}_\infty$).

Polynomial.trailingDegree_C theorem

(ha : a ≠ 0) : trailingDegree (C a) = (0 : ℕ∞)

Full source

@[simp]
theorem trailingDegree_C (ha : a ≠ 0) : trailingDegree (C a) = (0 : ℕ∞) :=
  trailingDegree_monomial ha

Trailing degree of constant polynomial: $\text{trailingDegree}(a) = 0$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$, the trailing degree of the constant polynomial $a$ (i.e., $C(a) \in R[X]$) is equal to $0$ (as an extended natural number).

Polynomial.le_trailingDegree_C theorem

: (0 : ℕ∞) ≤ trailingDegree (C a)

Full source

theorem le_trailingDegree_C : (0 : ℕ∞) ≤ trailingDegree (C a) :=
  le_trailingDegree_monomial

Lower Bound on Trailing Degree of Constant Polynomial: $\text{trailingDegree}(C(a)) \geq 0$

Informal description

For any element $a$ in a semiring $R$, the trailing degree of the constant polynomial $C(a) \in R[X]$ is bounded below by $0$ in the extended natural numbers $\mathbb{N}_\infty$, i.e., $0 \leq \text{trailingDegree}(C(a))$.

Polynomial.trailingDegree_one_le theorem

: (0 : ℕ∞) ≤ trailingDegree (1 : R[X])

Full source

theorem trailingDegree_one_le : (0 : ℕ∞) ≤ trailingDegree (1 : R[X]) := by
  rw [← C_1]
  exact le_trailingDegree_C

Lower Bound on Trailing Degree of the Unit Polynomial: $\text{trailingDegree}(1) \geq 0$

Informal description

For the constant polynomial $1$ in the polynomial ring $R[X]$, the trailing degree is bounded below by $0$ in the extended natural numbers $\mathbb{N}_\infty$, i.e., $0 \leq \text{trailingDegree}(1)$.

Polynomial.natTrailingDegree_C theorem

(a : R) : natTrailingDegree (C a) = 0

Full source

@[simp]
theorem natTrailingDegree_C (a : R) : natTrailingDegree (C a) = 0 :=
  nonpos_iff_eq_zero.1 natTrailingDegree_monomial_le

Natural Trailing Degree of Constant Polynomial is Zero

Informal description

For any element $a$ in a semiring $R$, the natural trailing degree of the constant polynomial $C(a) \in R[X]$ is zero, i.e., $\text{natTrailingDegree}(C(a)) = 0$.

Polynomial.natTrailingDegree_one theorem

: natTrailingDegree (1 : R[X]) = 0

Full source

@[simp]
theorem natTrailingDegree_one : natTrailingDegree (1 : R[X]) = 0 :=
  natTrailingDegree_C 1

Natural Trailing Degree of the Unit Polynomial is Zero

Informal description

For the constant polynomial $1$ in the polynomial ring $R[X]$, the natural trailing degree is zero, i.e., $\text{natTrailingDegree}(1) = 0$.

Polynomial.natTrailingDegree_natCast theorem

(n : ℕ) : natTrailingDegree (n : R[X]) = 0

Full source

@[simp]
theorem natTrailingDegree_natCast (n : ℕ) : natTrailingDegree (n : R[X]) = 0 := by
  simp only [← C_eq_natCast, natTrailingDegree_C]

Natural Trailing Degree of Constant Natural Number Polynomial is Zero

Informal description

For any natural number $n$, the natural trailing degree of the polynomial $n \in R[X]$ (interpreted as a constant polynomial) is zero, i.e., $\text{natTrailingDegree}(n) = 0$.

Polynomial.trailingDegree_C_mul_X_pow theorem

(n : ℕ) (ha : a ≠ 0) : trailingDegree (C a * X ^ n) = n

Full source

@[simp]
theorem trailingDegree_C_mul_X_pow (n : ℕ) (ha : a ≠ 0) : trailingDegree (C a * X ^ n) = n := by
  rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]

Trailing Degree of Monomial: $\text{trailingDegree}(a X^n) = n$ for $a \neq 0$

Informal description

For any natural number $n$ and any nonzero element $a$ in a semiring $R$, the trailing degree of the polynomial $a X^n$ is equal to $n$. That is, $\text{trailingDegree}(a X^n) = n$.

Polynomial.le_trailingDegree_C_mul_X_pow theorem

(n : ℕ) (a : R) : (n : ℕ∞) ≤ trailingDegree (C a * X ^ n)

Full source

theorem le_trailingDegree_C_mul_X_pow (n : ℕ) (a : R) :
    (n : ℕ∞) ≤ trailingDegree (C a * X ^ n) := by
  rw [C_mul_X_pow_eq_monomial]
  exact le_trailingDegree_monomial

Lower Bound on Trailing Degree of Monomial: $\text{trailingDegree}(a X^n) \geq n$

Informal description

For any natural number $n$ and any element $a$ in a semiring $R$, the trailing degree of the polynomial $a X^n$ is at least $n$. In other words, $\text{trailingDegree}(a X^n) \geq n$.

Polynomial.coeff_eq_zero_of_lt_trailingDegree theorem

(h : (n : ℕ∞) < trailingDegree p) : coeff p n = 0

Full source

theorem coeff_eq_zero_of_lt_trailingDegree (h : (n : ℕ∞) < trailingDegree p) : coeff p n = 0 :=
  Classical.not_not.1 (mt trailingDegree_le_of_ne_zero (not_le_of_gt h))

Vanishing of Coefficients Below Trailing Degree: $\text{coeff}(p, n) = 0$ for $n < \text{trailingDegree}(p)$

Informal description

For a polynomial $p \in R[X]$ and an extended natural number $n \in \mathbb{N}_\infty$, if $n$ is strictly less than the trailing degree of $p$ (i.e., $n < \text{trailingDegree}(p)$), then the coefficient of $X^n$ in $p$ is zero (i.e., $\text{coeff}(p, n) = 0$).

Polynomial.coeff_eq_zero_of_lt_natTrailingDegree theorem

{p : R[X]} {n : ℕ} (h : n < p.natTrailingDegree) : p.coeff n = 0

Full source

theorem coeff_eq_zero_of_lt_natTrailingDegree {p : R[X]} {n : ℕ} (h : n < p.natTrailingDegree) :
    p.coeff n = 0 := by
  apply coeff_eq_zero_of_lt_trailingDegree
  by_cases hp : p = 0
  · rw [hp, trailingDegree_zero]
    exact WithTop.coe_lt_top n
  · rw [trailingDegree_eq_natTrailingDegree hp]
    exact WithTop.coe_lt_coe.2 h

Vanishing of Coefficients Below Natural Trailing Degree: $\text{coeff}(p, n) = 0$ for $n < \text{natTrailingDegree}(p)$

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, if $n$ is strictly less than the natural trailing degree of $p$ (i.e., $n < \text{natTrailingDegree}(p)$), then the coefficient of $X^n$ in $p$ is zero (i.e., $\text{coeff}(p, n) = 0$).

Polynomial.coeff_natTrailingDegree_pred_eq_zero theorem

{p : R[X]} {hp : (0 : ℕ∞) < natTrailingDegree p} : p.coeff (p.natTrailingDegree - 1) = 0

Full source

@[simp]
theorem coeff_natTrailingDegree_pred_eq_zero {p : R[X]} {hp : (0 : ℕ∞) < natTrailingDegree p} :
    p.coeff (p.natTrailingDegree - 1) = 0 :=
  coeff_eq_zero_of_lt_natTrailingDegree <|
    Nat.sub_lt (WithTop.coe_pos.mp hp) Nat.one_pos

Vanishing of Coefficient at Predecessor of Natural Trailing Degree: $\text{coeff}(p, \text{natTrailingDegree}(p) - 1) = 0$

Informal description

For any polynomial $p \in R[X]$ with a positive natural trailing degree (i.e., $\text{natTrailingDegree}(p) > 0$), the coefficient of the term $X^{\text{natTrailingDegree}(p) - 1}$ is zero, i.e., $\text{coeff}(p, \text{natTrailingDegree}(p) - 1) = 0$.

Polynomial.le_trailingDegree_X_pow theorem

(n : ℕ) : (n : ℕ∞) ≤ trailingDegree (X ^ n : R[X])

Full source

theorem le_trailingDegree_X_pow (n : ℕ) : (n : ℕ∞) ≤ trailingDegree (X ^ n : R[X]) := by
  simpa only [C_1, one_mul] using le_trailingDegree_C_mul_X_pow n (1 : R)

Lower Bound on Trailing Degree of $X^n$: $\text{trailingDegree}(X^n) \geq n$

Informal description

For any natural number $n$, the trailing degree of the polynomial $X^n$ in the polynomial ring $R[X]$ is at least $n$ when viewed in the extended natural numbers $\mathbb{N}_\infty$. That is, $\text{trailingDegree}(X^n) \geq n$.

Polynomial.le_trailingDegree_X theorem

: (1 : ℕ∞) ≤ trailingDegree (X : R[X])

Full source

theorem le_trailingDegree_X : (1 : ℕ∞) ≤ trailingDegree (X : R[X]) :=
  le_trailingDegree_monomial

Lower Bound on Trailing Degree of $X$: $\text{trailingDegree}(X) \geq 1$

Informal description

For the polynomial variable $X$ in the polynomial ring $R[X]$, the trailing degree of $X$ is at least $1$ (when viewed in the extended natural numbers $\mathbb{N}_\infty$). That is, $\text{trailingDegree}(X) \geq 1$.

Polynomial.natTrailingDegree_X_le theorem

: (X : R[X]).natTrailingDegree ≤ 1

Full source

theorem natTrailingDegree_X_le : (X : R[X]).natTrailingDegree ≤ 1 :=
  natTrailingDegree_monomial_le

Upper bound on natural trailing degree of $X$: $\text{natTrailingDegree}(X) \leq 1$

Informal description

For the polynomial variable $X$ in the polynomial ring $R[X]$, the natural trailing degree satisfies $\text{natTrailingDegree}(X) \leq 1$.

Polynomial.trailingCoeff_eq_zero theorem

: trailingCoeff p = 0 ↔ p = 0

Full source

@[simp]
theorem trailingCoeff_eq_zero : trailingCoefftrailingCoeff p = 0 ↔ p = 0 :=
  ⟨fun h =>
    _root_.by_contradiction fun hp =>
      mt mem_support_iff.1 (Classical.not_not.2 h)
        (mem_of_min (trailingDegree_eq_natTrailingDegree hp)),
    fun h => h.symm ▸ leadingCoeff_zero⟩

Trailing Coefficient Vanishes if and only if Polynomial is Zero

Informal description

For a polynomial $p \in R[X]$, the trailing coefficient of $p$ is zero if and only if $p$ is the zero polynomial. That is, $\text{trailingCoeff}(p) = 0 \leftrightarrow p = 0$.

Polynomial.trailingCoeff_nonzero_iff_nonzero theorem

: trailingCoeff p ≠ 0 ↔ p ≠ 0

Full source

theorem trailingCoeff_nonzero_iff_nonzero : trailingCoefftrailingCoeff p ≠ 0trailingCoeff p ≠ 0 ↔ p ≠ 0 :=
  not_congr trailingCoeff_eq_zero

Nonzero Trailing Coefficient Characterizes Nonzero Polynomials

Informal description

For a polynomial $p \in R[X]$, the trailing coefficient of $p$ is nonzero if and only if $p$ is not the zero polynomial. That is, $\text{trailingCoeff}(p) \neq 0 \leftrightarrow p \neq 0$.

Polynomial.natTrailingDegree_mem_support_of_nonzero theorem

: p ≠ 0 → natTrailingDegree p ∈ p.support

Full source

theorem natTrailingDegree_mem_support_of_nonzero : p ≠ 0 → natTrailingDegreenatTrailingDegree p ∈ p.support :=
  mem_support_iffmem_support_iff.mpr ∘ trailingCoeff_nonzero_iff_nonzero.mpr

Nonzero Polynomials Have Trailing Degree in Their Support

Informal description

For any nonzero polynomial $p \in R[X]$, the natural trailing degree of $p$ belongs to the support of $p$, i.e., the coefficient of $X^{\text{natTrailingDegree}(p)}$ in $p$ is nonzero.

Polynomial.natTrailingDegree_le_of_mem_supp theorem

(a : ℕ) : a ∈ p.support → natTrailingDegree p ≤ a

Full source

theorem natTrailingDegree_le_of_mem_supp (a : ℕ) : a ∈ p.support → natTrailingDegree p ≤ a :=
  natTrailingDegree_le_of_ne_zeronatTrailingDegree_le_of_ne_zero ∘ mem_support_iff.mp

Natural Trailing Degree Bound for Exponents in Support: $\text{natTrailingDegree}(p) \leq a$ when $p_a \neq 0$

Informal description

For any polynomial $p \in R[X]$ and natural number $a$, if $a$ belongs to the support of $p$ (i.e., the coefficient of $X^a$ in $p$ is nonzero), then the natural trailing degree of $p$ is less than or equal to $a$.

Polynomial.natTrailingDegree_eq_support_min' theorem

(h : p ≠ 0) : natTrailingDegree p = p.support.min' (nonempty_support_iff.mpr h)

Full source

theorem natTrailingDegree_eq_support_min' (h : p ≠ 0) :
    natTrailingDegree p = p.support.min' (nonempty_support_iff.mpr h) := by
  rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]

Natural Trailing Degree Equals Minimum Exponent in Support for Nonzero Polynomials

Informal description

For any nonzero polynomial $p \in R[X]$, the natural trailing degree of $p$ is equal to the minimum exponent in the support of $p$, i.e., $$\text{natTrailingDegree}(p) = \min \{n \in \mathbb{N} \mid \text{coeff}_n(p) \neq 0\}.$$

Polynomial.le_natTrailingDegree theorem

(hp : p ≠ 0) (hn : ∀ m < n, p.coeff m = 0) : n ≤ p.natTrailingDegree

Full source

theorem le_natTrailingDegree (hp : p ≠ 0) (hn : ∀ m < n, p.coeff m = 0) :
    n ≤ p.natTrailingDegree := by
  rw [natTrailingDegree_eq_support_min' hp]
  exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn

Lower Bound on Natural Trailing Degree of Nonzero Polynomials

Informal description

For any nonzero polynomial $p \in R[X]$ and natural number $n$, if all coefficients of $p$ with degree less than $n$ are zero (i.e., $p_m = 0$ for all $m < n$), then $n$ is less than or equal to the natural trailing degree of $p$, i.e., $n \leq \text{natTrailingDegree}(p)$.

Polynomial.natTrailingDegree_le_natDegree theorem

(p : R[X]) : p.natTrailingDegree ≤ p.natDegree

Full source

theorem natTrailingDegree_le_natDegree (p : R[X]) : p.natTrailingDegree ≤ p.natDegree := by
  by_cases hp : p = 0
  · rw [hp, natDegree_zero, natTrailingDegree_zero]
  · exact le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)

Natural Trailing Degree Bounded by Natural Degree in Polynomials

Informal description

For any polynomial $p \in R[X]$, the natural trailing degree of $p$ is less than or equal to its natural degree, i.e., $$\text{natTrailingDegree}(p) \leq \text{natDegree}(p).$$

Polynomial.natTrailingDegree_mul_X_pow theorem

{p : R[X]} (hp : p ≠ 0) (n : ℕ) : (p * X ^ n).natTrailingDegree = p.natTrailingDegree + n

Full source

theorem natTrailingDegree_mul_X_pow {p : R[X]} (hp : p ≠ 0) (n : ℕ) :
    (p * X ^ n).natTrailingDegree = p.natTrailingDegree + n := by
  apply le_antisymm
  · refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_
    rwa [trailingCoeff, ← coeff_mul_X_pow]
  · rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]
    intro y hy
    have key : n ≤ y := by
      rw [mem_support_iff, coeff_mul_X_pow'] at hy
      exact by_contra fun h => hy (if_neg h)
    rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy
    exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)

Natural Trailing Degree Shift Formula for Polynomial Multiplication by $X^n$

Informal description

For any nonzero polynomial $p \in R[X]$ over a semiring $R$ and any natural number $n$, the natural trailing degree of the product $p \cdot X^n$ is equal to the sum of the natural trailing degree of $p$ and $n$, i.e., $$\text{natTrailingDegree}(p \cdot X^n) = \text{natTrailingDegree}(p) + n.$$

Polynomial.le_trailingDegree_mul theorem

: p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Full source

theorem le_trailingDegree_mul : p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree := by
  refine Finset.le_min fun n hn => ?_
  rw [mem_support_iff, coeff_mul] at hn
  obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn
  refine
    (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
          (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans_eq ?_
  rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← mem_antidiagonal]

Sum of Trailing Degrees Bounded by Trailing Degree of Product

Informal description

For any two polynomials $p, q \in R[X]$ over a semiring $R$, the sum of their trailing degrees is less than or equal to the trailing degree of their product, i.e., $$\text{trailingDegree}(p) + \text{trailingDegree}(q) \leq \text{trailingDegree}(p \cdot q).$$

Polynomial.le_natTrailingDegree_mul theorem

(h : p * q ≠ 0) : p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

Full source

theorem le_natTrailingDegree_mul (h : p * q ≠ 0) :
    p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree := by
  have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])
  have hq : q ≠ 0 := fun hq => h (by rw [hq, mul_zero])
  rw [← WithTop.coe_le_coe, WithTop.coe_add, ← Nat.cast_withTop (natTrailingDegree p),
    ← Nat.cast_withTop (natTrailingDegree q), ← Nat.cast_withTop (natTrailingDegree (p * q)),
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq,
    ← trailingDegree_eq_natTrailingDegree h]
  exact le_trailingDegree_mul

Sum of Natural Trailing Degrees Bounded by Natural Trailing Degree of Product

Informal description

For any two polynomials $p, q \in R[X]$ over a semiring $R$ such that their product $p \cdot q$ is nonzero, the sum of their natural trailing degrees is less than or equal to the natural trailing degree of their product, i.e., $$\text{natTrailingDegree}(p) + \text{natTrailingDegree}(q) \leq \text{natTrailingDegree}(p \cdot q).$$

Polynomial.coeff_mul_natTrailingDegree_add_natTrailingDegree theorem

: (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff

Full source

theorem coeff_mul_natTrailingDegree_add_natTrailingDegree : (p * q).coeff
    (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff := by
  rw [coeff_mul]
  refine
    Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) ?_ fun h =>
      (h (mem_antidiagonal.mpr rfl)).elim
  rintro ⟨i, j⟩ h₁ h₂
  rw [mem_antidiagonal] at h₁
  by_cases hi : i < p.natTrailingDegree
  · rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]
  by_cases hj : j < q.natTrailingDegree
  · rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]
  rw [not_lt] at hi hj
  refine (h₂ (Prod.ext_iff.mpr ?_).symm).elim
  exact (add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm

Product of Trailing Coefficients in Polynomial Multiplication: $(p \cdot q)_{n+m} = p_n \cdot q_m$

Informal description

For any two nonzero polynomials $p, q \in R[X]$ over a semiring $R$, the coefficient of the term $X^{n+m}$ in the product $p \cdot q$ (where $n = \text{natTrailingDegree}(p)$ and $m = \text{natTrailingDegree}(q)$) is equal to the product of the trailing coefficients of $p$ and $q$. That is, $$(p \cdot q)_{n+m} = p_n \cdot q_m.$$

Polynomial.trailingDegree_mul' theorem

(h : p.trailingCoeff * q.trailingCoeff ≠ 0) : (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Full source

theorem trailingDegree_mul' (h : p.trailingCoeff * q.trailingCoeff ≠ 0) :
    (p * q).trailingDegree = p.trailingDegree + q.trailingDegree := by
  have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
  have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
  refine le_antisymm ?_ le_trailingDegree_mul
  rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ←
    ENat.coe_add]
  apply trailingDegree_le_of_ne_zero
  rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]

Trailing Degree Additivity for Polynomial Multiplication with Nonzero Trailing Coefficients

Informal description

For two polynomials $p, q \in R[X]$ over a semiring $R$, if the product of their trailing coefficients is nonzero (i.e., $\text{trailingCoeff}(p) \cdot \text{trailingCoeff}(q) \neq 0$), then the trailing degree of their product is equal to the sum of their trailing degrees, i.e., $$\text{trailingDegree}(p \cdot q) = \text{trailingDegree}(p) + \text{trailingDegree}(q).$$

Polynomial.natTrailingDegree_mul' theorem

(h : p.trailingCoeff * q.trailingCoeff ≠ 0) : (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Full source

theorem natTrailingDegree_mul' (h : p.trailingCoeff * q.trailingCoeff ≠ 0) :
    (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree := by
  have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
  have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
  apply natTrailingDegree_eq_of_trailingDegree_eq_some
  rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]

Additivity of Natural Trailing Degree for Polynomial Multiplication with Nonzero Trailing Coefficients

Informal description

For two polynomials $p, q \in R[X]$ over a semiring $R$, if the product of their trailing coefficients is nonzero (i.e., $\text{trailingCoeff}(p) \cdot \text{trailingCoeff}(q) \neq 0$), then the natural trailing degree of their product is equal to the sum of their natural trailing degrees, i.e., $$\text{natTrailingDegree}(p \cdot q) = \text{natTrailingDegree}(p) + \text{natTrailingDegree}(q).$$

Polynomial.natTrailingDegree_mul theorem

 [NoZeroDivisors R] (hp : p ≠ 0) (hq : q ≠ 0) : (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Full source

theorem natTrailingDegree_mul [NoZeroDivisors R] (hp : p ≠ 0) (hq : q ≠ 0) :
    (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree :=
  natTrailingDegree_mul'
    (mul_ne_zero (mt trailingCoeff_eq_zero.mp hp) (mt trailingCoeff_eq_zero.mp hq))

Additivity of Natural Trailing Degree for Nonzero Polynomials over a Semiring with No Zero Divisors

Informal description

Let $R$ be a semiring with no zero divisors, and let $p, q \in R[X]$ be nonzero polynomials. Then the natural trailing degree of the product $p \cdot q$ is the sum of the natural trailing degrees of $p$ and $q$, i.e., $$\text{natTrailingDegree}(p \cdot q) = \text{natTrailingDegree}(p) + \text{natTrailingDegree}(q).$$

Polynomial.trailingDegree_one theorem

: trailingDegree (1 : R[X]) = (0 : ℕ∞)

Full source

@[simp]
theorem trailingDegree_one : trailingDegree (1 : R[X]) = (0 : ℕ∞) :=
  trailingDegree_C one_ne_zero

Trailing Degree of the Unit Polynomial: $\text{trailingDegree}(1) = 0$

Informal description

The trailing degree of the constant polynomial $1$ in the polynomial ring $R[X]$ is $0$ (as an extended natural number), i.e., $\text{trailingDegree}(1) = 0$.

Polynomial.trailingDegree_X theorem

: trailingDegree (X : R[X]) = 1

Full source

@[simp]
theorem trailingDegree_X : trailingDegree (X : R[X]) = 1 :=
  trailingDegree_monomial one_ne_zero

Trailing Degree of $X$: $\text{trailingDegree}(X) = 1$

Informal description

For the polynomial variable $X$ in the polynomial ring $R[X]$, the trailing degree is equal to $1$, i.e., $\text{trailingDegree}(X) = 1$.

Polynomial.natTrailingDegree_X theorem

: (X : R[X]).natTrailingDegree = 1

Full source

@[simp]
theorem natTrailingDegree_X : (X : R[X]).natTrailingDegree = 1 :=
  natTrailingDegree_monomial one_ne_zero

Natural Trailing Degree of $X$: $\text{natTrailingDegree}(X) = 1$

Informal description

For the polynomial variable $X$ in the polynomial ring $R[X]$, the natural trailing degree is equal to $1$, i.e., $\text{natTrailingDegree}(X) = 1$.

Polynomial.trailingDegree_X_pow theorem

(n : ℕ) : (X ^ n : R[X]).trailingDegree = n

Full source

@[simp]
lemma trailingDegree_X_pow (n : ℕ) :
    (X ^ n : R[X]).trailingDegree = n := by
  rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]

Trailing degree of $X^n$: $\text{trailingDegree}(X^n) = n$

Informal description

For any natural number $n$, the trailing degree of the polynomial $X^n$ in the ring $R[X]$ is equal to $n$.

Polynomial.natTrailingDegree_X_pow theorem

(n : ℕ) : (X ^ n : R[X]).natTrailingDegree = n

Full source

@[simp]
lemma natTrailingDegree_X_pow (n : ℕ) :
    (X ^ n : R[X]).natTrailingDegree = n := by
  rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]

Natural Trailing Degree of $X^n$: $\text{natTrailingDegree}(X^n) = n$

Informal description

For any natural number $n$, the natural trailing degree of the polynomial $X^n$ in the ring $R[X]$ is equal to $n$, i.e., $\text{natTrailingDegree}(X^n) = n$.

Polynomial.trailingDegree_neg theorem

(p : R[X]) : trailingDegree (-p) = trailingDegree p

Full source

@[simp]
theorem trailingDegree_neg (p : R[X]) : trailingDegree (-p) = trailingDegree p := by
  unfold trailingDegree
  rw [support_neg]

Trailing Degree Invariance under Negation: $\text{trailingDegree}(-p) = \text{trailingDegree}(p)$

Informal description

For any polynomial $p \in R[X]$ over a ring $R$, the trailing degree of the negated polynomial $-p$ is equal to the trailing degree of $p$. That is, $\text{trailingDegree}(-p) = \text{trailingDegree}(p)$.

Polynomial.natTrailingDegree_neg theorem

(p : R[X]) : natTrailingDegree (-p) = natTrailingDegree p

Full source

@[simp]
theorem natTrailingDegree_neg (p : R[X]) : natTrailingDegree (-p) = natTrailingDegree p := by
  simp [natTrailingDegree]

Natural Trailing Degree Invariance under Negation: $\text{natTrailingDegree}(-p) = \text{natTrailingDegree}(p)$

Informal description

For any polynomial $p \in R[X]$ over a ring $R$, the natural trailing degree of the negated polynomial $-p$ is equal to the natural trailing degree of $p$. That is, $\text{natTrailingDegree}(-p) = \text{natTrailingDegree}(p)$.

Polynomial.natTrailingDegree_intCast theorem

(n : ℤ) : natTrailingDegree (n : R[X]) = 0

Full source

@[simp]
theorem natTrailingDegree_intCast (n : ℤ) : natTrailingDegree (n : R[X]) = 0 := by
  simp only [← C_eq_intCast, natTrailingDegree_C]

Natural Trailing Degree of Integer Constant Polynomial is Zero

Informal description

For any integer $n \in \mathbb{Z}$, the natural trailing degree of the constant polynomial $n \in R[X]$ is zero, i.e., $\text{natTrailingDegree}(n) = 0$.

Polynomial.nextCoeffUp definition

(p : R[X]) : R

Full source

/-- The second-lowest coefficient, or 0 for constants -/
def nextCoeffUp (p : R[X]) : R :=
  if p.natTrailingDegree = 0 then 0 else p.coeff (p.natTrailingDegree + 1)

Next coefficient above trailing term

Informal description

For a polynomial $ p \in R[X] $, the function $\text{nextCoeffUp}(p)$ returns the coefficient of the term $ X^{n+1} $ where $ n $ is the natural trailing degree of $ p $. If $ p $ has no trailing term (i.e., $ n = 0 $), the function returns $ 0 $. More precisely: \[ \text{nextCoeffUp}(p) = \begin{cases} 0 & \text{if } \text{natTrailingDegree}(p) = 0, \\ p_{\text{natTrailingDegree}(p) + 1} & \text{otherwise}, \end{cases} \] where $ p_k $ denotes the coefficient of $ X^k $ in $ p $.

Polynomial.nextCoeffUp_zero theorem

: nextCoeffUp (0 : R[X]) = 0

Full source

@[simp] lemma nextCoeffUp_zero : nextCoeffUp (0 : R[X]) = 0 := by simp [nextCoeffUp]

Next Coefficient Above Trailing Term of Zero Polynomial is Zero

Informal description

For the zero polynomial $0 \in R[X]$, the next coefficient above the trailing term is zero, i.e., $\text{nextCoeffUp}(0) = 0$.

Polynomial.nextCoeffUp_C_eq_zero theorem

(c : R) : nextCoeffUp (C c) = 0

Full source

@[simp]
theorem nextCoeffUp_C_eq_zero (c : R) : nextCoeffUp (C c) = 0 := by
  rw [nextCoeffUp]
  simp

Next Coefficient Above Trailing Term Vanishes for Constant Polynomials

Informal description

For any constant polynomial $C(c) \in R[X]$ where $c \in R$, the next coefficient above the trailing term is zero, i.e., $\text{nextCoeffUp}(C(c)) = 0$.

Polynomial.nextCoeffUp_of_constantCoeff_eq_zero theorem

(p : R[X]) (hp : coeff p 0 = 0) : nextCoeffUp p = p.coeff (p.natTrailingDegree + 1)

Full source

theorem nextCoeffUp_of_constantCoeff_eq_zero (p : R[X]) (hp : coeff p 0 = 0) :
    nextCoeffUp p = p.coeff (p.natTrailingDegree + 1) := by
  obtain rfl | hp₀ := eq_or_ne p 0
  · simp
  · rw [nextCoeffUp, if_neg (natTrailingDegree_ne_zero.2 ⟨hp₀, hp⟩)]

Next Coefficient Above Trailing Term for Polynomials with Zero Constant Term

Informal description

For a polynomial $p \in R[X]$ with zero constant term (i.e., $\text{coeff}(p, 0) = 0$), the next coefficient above the trailing term is equal to the coefficient of $X^{n+1}$, where $n$ is the natural trailing degree of $p$. That is, \[ \text{nextCoeffUp}(p) = p_{n+1}, \] where $n = \text{natTrailingDegree}(p)$ and $p_k$ denotes the coefficient of $X^k$ in $p$.

Polynomial.coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt theorem

(h : trailingDegree p < trailingDegree q) : coeff q (natTrailingDegree p) = 0

Full source

theorem coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt
    (h : trailingDegree p < trailingDegree q) : coeff q (natTrailingDegree p) = 0 :=
  coeff_eq_zero_of_lt_trailingDegree <| natTrailingDegree_le_trailingDegree.trans_lt h

Vanishing Coefficient at Natural Trailing Degree under Trailing Degree Comparison

Informal description

For polynomials $p, q \in R[X]$, if the trailing degree of $p$ is strictly less than the trailing degree of $q$, then the coefficient of $q$ at the natural trailing degree of $p$ is zero, i.e., $\text{coeff}(q, \text{natTrailingDegree}(p)) = 0$.

Polynomial.ne_zero_of_trailingDegree_lt theorem

{n : ℕ∞} (h : trailingDegree p < n) : p ≠ 0

Full source

theorem ne_zero_of_trailingDegree_lt {n : ℕ∞} (h : trailingDegree p < n) : p ≠ 0 := fun h₀ =>
  h.not_le (by simp [h₀])

Nonzero Polynomial When Trailing Degree is Bounded Below

Informal description

For any polynomial $p \in R[X]$ and extended natural number $n \in \mathbb{N}_\infty$, if the trailing degree of $p$ is strictly less than $n$, then $p$ is not the zero polynomial.

Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero theorem

(h : constantCoeff p ≠ 0) : p.natTrailingDegree = 0

Full source

lemma natTrailingDegree_eq_zero_of_constantCoeff_ne_zero (h : constantCoeffconstantCoeff p ≠ 0) :
    p.natTrailingDegree = 0 :=
  le_antisymm (natTrailingDegree_le_of_ne_zero h) zero_le'

Natural Trailing Degree is Zero for Nonzero Constant Term Polynomials

Informal description

For a polynomial $p \in R[X]$, if the constant term of $p$ is nonzero (i.e., $\text{constantCoeff}(p) \neq 0$), then the natural trailing degree of $p$ is zero (i.e., $\text{natTrailingDegree}(p) = 0$).

Main definitions