nextCoeffUp — Mathlib

English

If the constant term of p is zero, then nextCoeffUp p equals the coefficient at the next degree: nextCoeffUp p = coeff(p, natTrailingDegree(p) + 1).

Русский

Если константный коэффициент p равен нулю, то nextCoeffUp p равна коэффициенту при следующей степени: nextCoeffUp p = coeff(p, natTrailingDegree(p) + 1).

LaTeX

$$$ \text{coeff}(p, \operatorname{natTrailingDegree}(p) + 1) $$$

Lean4

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

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