nextCoeff — Mathlib

English

The second-highest coefficient of a polynomial p is given by nextCoeff(p), i.e., the coefficient of degree natDegree(p) − 1 unless p is constant.

Русский

Вычисление второго по величине коэффициента многочлена p задаётся через nextCoeff(p): коэффициент при степени natDegree(p) − 1, если p не константа.

LaTeX

$${R : Type u} → [Semiring R] → Polynomial R → R : nextCoeff(p) = if natDegree(p) = 0 then 0 else coeff(p, natDegree(p) - 1)$$

Lean4

/-- The second-highest coefficient, or 0 for constants -/
def nextCoeff (p : R[X]) : R :=
  if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)

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