coeff_apply

Mathlib.RingTheory.MvPowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.coeff_apply

English

For any f and index d, the nth coefficient of f equals the value f at d: coeff d f = f d.

Русский

Для любой $f$ и индекса $d$ коэффициент $d$ равен значению $f$ в точке $d$: $\\mathrm{coeff}_d f = f(d)$.

LaTeX

$$$\\operatorname{coeff}(d)\\, f = f(d)$$$

Lean4

theorem coeff_apply (f : MvPowerSeries σ R) (d : σ →₀ ℕ) : coeff d f = f d :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru