natDegree — Mathlib

English

natDegree(p) is the natural degree of p, defined as the natural value of degree(p); natDegree(0) = 0.

Русский

natDegree(p) — натуральная степень p, определяемая как естественное число, соответствующее degree(p); natDegree(0) = 0.

LaTeX

$$$\operatorname{natDegree}(p) = \begin{cases} \operatorname{degree}(p) & \text{if } \operatorname{degree}(p) \neq \bot, \\ 0 & \text{if } p = 0. \end{cases}$$$

Lean4

/-- `natDegree p` forces `degree p` to ℕ, by defining `natDegree 0 = 0`. -/
def natDegree (p : R[X]) : ℕ :=
  (degree p).unbotD 0

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