cuspFunction_apply_zero — Mathlib

English

For NeZero n and CuspFormClass data, cuspFunction n f 0 = 0; the cuspFunction vanishes at zero for cusp forms.

Русский

Для непустого n и данных CuspFormClass, cuspFunction n f 0 = 0; cuspFunction обращается к нулю в нуле для к cuspForms.

LaTeX

$$$\text{cuspFunction } n\, f(0) = 0$$$

Lean4

theorem cuspFunction_apply_zero [NeZero n] [CuspFormClass F Γ(n) k] : cuspFunction n f 0 = 0 :=
  Periodic.cuspFunction_zero_of_zero_at_inf (mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _)))
    (zero_at_infty_comp_ofComplex f)

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