petersson_smul — Mathlib

English

For SL(2,ℤ) the same invariance statement holds as in GL case; the slash action reduces to the standard modular slash on the upper half-plane.

Русский

Для SL(2,ℤ) сохранение тождества аналогично случая GL; действие слэш соответствует обычному модулярному слэшу на верхней полуплоскости.

LaTeX

$$$\mathrm{petersson}_k\bigl( f|[k]g, f'|[k]g \bigr)(\tau) = \mathrm{petersson}_k(f,f')(g\cdot \tau)\quad (g\in SL(2,\mathbb{Z}))$$$

Lean4

theorem petersson_smul {k g τ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [SlashInvariantFormClass F Γ k] {f : F}
    [SlashInvariantFormClass F' Γ k] {f' : F'} (hg : g ∈ Γ) : petersson k f f' (g • τ) = petersson k f f' τ := by
  simpa [SlashInvariantFormClass.slash_action_eq _ _ hg, Subgroup.HasDetOne.det_eq hg, σ] using
    (petersson_slash k f f' g τ).symm

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