slash_def — Mathlib

English

There is a weight-k slash action of ℤ on SL(2, ℤ) on functions f: 𝔥 → ℂ, obtained by transporting the real GL2 action via mapGL.

Русский

Существует slash-действие веса k ℤ над SL(2,ℤ) на функции f: ℍ → ℂ, получаемое переводом через отображение mapGL.

LaTeX

$$$\text{SlashAction}_{k} : SL(2, \mathbb{Z}) \curvearrowright (\mathcal{H} \to \mathbb{C})$$$

Lean4

theorem slash_def (g : GL (Fin 2) ℝ) : f ∣[k] g = fun τ ↦ σ g (f (g • τ)) * |g.det.val| ^ (k - 1) * denom g τ ^ (-k) :=
  rfl

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