English
The trailing degree of a polynomial is the smallest exponent with a nonzero coefficient; equivalently, the minimal index in the support of p; trailingDegree(0) = ∞.
Русский
Степень пограничной минимальной степени полинома — наименьшая экспонента с ненулевым коэффициентом; для p ≠ 0 это минимальный элемент в поддержке p; trailingDegree(0) = ∞.
LaTeX
$$$\operatorname{trailingDegree}(p) = \min\operatorname{supp}(p) \quad(\text{и } \operatorname{trailingDegree}(0)=\infty).$$$
Lean4
/-- `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
