coeff_eq_ncoeff — Mathlib

English

Coefficient map equals the ncoeff map evaluated at each index, i.e., HVertexOperator.coeff A n = A[[-n - 1]].

Русский

Коэффициентная карта равна ncoeff(A) на индексе, то есть HVertexOperator.coeff A n = A[[-n - 1]].

LaTeX

$$$HVertexOperator.coeff\ A\ n = A[[-n-1]]$$$

Lean4

@[simp]
theorem coeff_eq_ncoeff (A : VertexOperator R V) (n : ℤ) : HVertexOperator.coeff A n = A[[-n - 1]] := by
  rw [ncoeff_apply, neg_sub, Int.sub_neg, add_sub_cancel_left]

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