degree — Mathlib

English

The degree of p is the largest exponent n for which X^n appears in p; for p = 0, degree(p) = bottom (⊥).

Русский

Степень многочлена p равна наибольшему степенному показателю n, при котором встречается слагаемое X^n; для p = 0 степень равна ⊥.

LaTeX

$$$\deg(p) = \max \{ n \in \mathbb{N} \mid \operatorname{coeff}(p,n) \neq 0 \} ,\quad \deg(0) = \bot$$$

Lean4

/-- `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

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