ncoeff_apply

Mathlib.Algebra.Vertex.VertexOperator

URI: https://scilib.ai/kg/mathlib#VertexOperator.ncoeff_apply

English

For any VertexOperator A and integer n, ncoeff A n equals coeff A (-n − 1).

Русский

Для любого VertexOperator A и целого числа n выполняется ncoeff A n = coeff A(-n − 1).

LaTeX

$$$ncoeff\ A\ n = coeff\ A(-n-1)$$$

Lean4

theorem ncoeff_apply (A : VertexOperator R V) (n : ℤ) : ncoeff A n = coeff A (-n - 1) :=
  rfl

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

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

Разделы

Аффилиация

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