natTrailingDegree — Mathlib

English

natTrailingDegree(p) is the natural number corresponding to trailingDegree(p) via ENat.toNat, i.e., natTrailingDegree(p) = ENat.toNat(trailingDegree(p)).

Русский

natTrailingDegree(p) есть натуральное число, получаемое из trailingDegree(p) через ENat.toNat: natTrailingDegree(p) = ENat.toNat(trailingDegree(p)).

LaTeX

$$$\operatorname{natTrailingDegree}(p) = \operatorname{ENat}.toNat(\operatorname{trailingDegree}(p)).$$$

Lean4

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

Похожие утверждения