is_invariant_const — Mathlib

English

There is an SL(2,ℤ)-slash action on SLInvariantForms, i.e., a weight-k slash action of SL(2,ℤ) on functions on the upper half-plane with respect to GL.

Русский

Существует slash-действие SL(2,ℤ) над SlashInvariantForm, то есть весового slash-действия SL(2,ℤ) на функции на верхней полуплоскости относительно GL.

LaTeX

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

Lean4

theorem is_invariant_const (A : SL(2, ℤ)) (x : ℂ) : Function.const ℍ x ∣[(0 : ℤ)] A = Function.const ℍ x :=
  by
  funext
  simp [SL_slash, slash_def, σ, zero_lt_one]

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