qExpansionFormalMultilinearSeries

English

There is a formal multilinear series qExpansionFormalMultilinearSeries n f which encodes the q-expansion coefficients via a canonical multilinear map.

Русский

Существует формальная многочестная линейная серия qExpansionFormalMultilinearSeries, кодирующая коэффициенты q-разложения через канонические многочлены.

LaTeX

$$$qExpansionFormalMultilinearSeries\; n\; f : \text{FormalMultilinearSeries } \mathbb{C} \mathbb{C} \mathbb{C}$$$

Lean4

/-- The `q`-expansion of a level `n` modular form, bundled as a `FormalMultilinearSeries`.

TODO: Maybe get rid of this and instead define a general API for converting `PowerSeries` to
`FormalMultilinearSeries`.
-/
def qExpansionFormalMultilinearSeries : FormalMultilinearSeries ℂ ℂ ℂ := fun m ↦
  (qExpansion n f).coeff m • ContinuousMultilinearMap.mkPiAlgebraFin ℂ m _

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