coeff

Mathlib.Analysis.Calculus.FormalMultilinearSeries

URI: https://scilib.ai/kg/mathlib#FormalMultilinearSeries.coeff

English

If n is strictly less than the order, then the coefficient p(n) vanishes: p(n) = 0 whenever n < p.order.

Русский

Если n < p.order, то коэффициент p(n) равен 0.

LaTeX

$$$n < p.\\mathrm{order} \\Rightarrow p(n) = 0$$$

Lean4

/-- The `n`th coefficient of `p` when seen as a power series. -/
def coeff (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : E :=
  p n 1

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

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

Разделы

Аффилиация

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