of_coeff_coeff — Mathlib

English

For a vertex operator A, applying of_coeff to its coefficient data with the PWO-support recovers A; i.e., A = of_coeff(A.coeff, A.coeff_isPWOsupport).

Русский

Для вершины-оператора A применение of_coeff к её коэффициентам и поддержке PWOn возвращает A; то есть A = of_coeff(A.coeff, A.coeff_isPWOsupport).

LaTeX

$$$ \operatorname{of\_coeff} (A.c\oe f f, A.c\oe f f\_isPWOsupp) = A $$$

Lean4

@[simp]
theorem of_coeff_coeff (A : HVertexOperator Γ R V W) : of_coeff A.coeff A.coeff_isPWOsupport = A :=
  rfl

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