compHahnSeries_smul — Mathlib

English

The composite of two heterogeneous vertex operators is again a heterogeneous vertex operator, with a product-type indexing reflecting the pair of orders.

Русский

Сложение двух гетерогенных вершинных операторов вновь образует гетерогенный вершинный оператор; индексирование отражает пару порядков.

LaTeX

$$$\mathrm{comp}: HVertexOperator(\Γ) \times HVertexOperator(\Γ') \to HVertexOperator(\mathrm{Lex}(\mathrm{Prod}(\Gamma',\Gamma)))$$$

Lean4

@[simp]
theorem compHahnSeries_smul (r : R) (u : U) : compHahnSeries A B (r • u) = r • compHahnSeries A B u :=
  by
  ext
  simp only [compHahnSeries_coeff, map_smul, coeff_apply_apply, HahnSeries.coeff_smul]
  rw [← HahnSeries.coeff_smul]

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