zero_at_infty_slash — Mathlib

English

Translating a cusp form by SL(2,ℤ) yields a cusp form with the transformed group.

Русский

Перенос cusp-формы по SL(2,ℤ) даёт cusp-форму для преобразованной группы.

LaTeX

$$$[\\text{CuspFormClass F Γ k}] (g) : CuspForm( toConjAct(g^{-1})·Γ, k)$ such that translation is compatible with SL(2,ℤ).$$

Lean4

theorem zero_at_infty_slash [CuspFormClass F Γ k] (f : F) (g : SL(2, ℤ)) : IsZeroAtImInfty (f ∣[k] g) :=
  by
  rw [← OnePoint.isZeroAt_infty_iff, SL_slash, ← OnePoint.IsZeroAt.smul_iff]
  apply zero_at_cusps f
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']
  exact ⟨g, by simp [mapGL]⟩

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