ncoeff — Mathlib

English

The ncoeff map for VertexOperator relates to the coefficient map by ncoeff(A)(n) = coeff(A)(-n-1).

Русский

Карта ncoeff для VertexOperator задаёт отношение: ncoeff(A)(n) = coeff(A)(-n-1).

LaTeX

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

Lean4

/-- The coefficient of a vertex operator under normalized indexing. -/
def ncoeff : VertexOperator R V →ₗ[R] ℤ → Module.End R V
    where
  toFun A n := HVertexOperator.coeff A (-n - 1)
  map_add' _ _ := by ext; simp
  map_smul' _ _ := by ext; simp

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