English
There is a weight-k slash action of GL(2, ℝ) on the space of functions f: 𝔥 → ℂ, i.e., SLASH operator defined for GL(2,ℝ) acts on functions on the upper half-plane with weight k.
Русский
Существует slash-действие веса k of GL(2, ℝ) на пространстве функций f: ℍ → ℂ; неравно-weight slash-действие действует на функции на верхней полуплоскости.
LaTeX
$$$\text{SlashAction}_{k, GL(2,\mathbb{R})}: SL(2,\mathbb{R}) \curvearrowright (\mathcal{H} \to \mathbb{C})$$$
Lean4
/-- The weight `k` action of `GL (Fin 2) ℝ` on functions `f : ℍ → ℂ`. -/
instance : SlashAction ℤ (GL (Fin 2) ℝ) (ℍ → ℂ)
where
map := privateSlash
zero_slash := zero_slash
slash_one := slash_one
slash_mul := slash_mul
add_slash := add_slash
