zero_at_infty — Mathlib

English

A cusp form translated by SL(2,ℤ) remains a cusp form for the SL(2,ℤ)-conjugated subgroup.

Русский

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

LaTeX

$$$\\text{Translate}_{SL2Z}: \\mathrm{CuspForm}(Γ) \\to \\mathrm{CuspForm}(SL2Z^{-1}Γ SL2Z)$, preserving cusp property.$$

Lean4

theorem zero_at_infty [CuspFormClass F Γ k] (f : F) : IsZeroAtImInfty f := by
  simpa using CuspFormClass.zero_at_infty_slash f 1

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