ncoeff_of_coeff — Mathlib

English

The n-th coefficient of VertexOperator.of_coeff f hf is exactly f(-n-1).

Русский

n-й коэффициент VertexOperator.of_coeff f hf равен f(-n-1).

LaTeX

$$$(\\mathrm{of\\_coeff}\\ f\\ hf) [[n]] = f(-n-1)$$$

Lean4

@[simp]
theorem ncoeff_of_coeff (f : ℤ → Module.End R V) (hf : ∀ (x : V), ∃ (n : ℤ), ∀ (m : ℤ), m < n → (f m) x = 0) (n : ℤ) :
    (of_coeff f hf)[[n]] = f (-n - 1) := by
  ext v
  rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]

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