coeff — Mathlib

English

The nth coefficient operator maps a multivariate power series to its nth coefficient.

Русский

Оператор коэффициента для индекса n отображает многомерную формальную степенную серию к её коэффициенту при n.

LaTeX

$$$\\mathrm{coeff}(n) : \\mathrm{MvPowerSeries}(\\sigma,R) \\to R$$$

Lean4

/-- The `n`th coefficient of a multivariate formal power series. -/
def coeff (n : σ →₀ ℕ) : MvPowerSeries σ R →ₗ[R] R :=
  LinearMap.proj n

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