instZero — Mathlib

English

There exists a zero modular form, whose values are identically zero on the upper half-plane and which has trivial holomorphy and cusp-boundedness properties.

Русский

Существует нулевая модульная форма, значение которой на всей верхней полуплоскости равно нулю, с тождественной голоморфностью и ограниченностью на бесконечностях.

LaTeX

$$$0 \in \mathrm{ModularForm}(\Gamma,k)$ with $(0)(z)=0$ for all $z$$$

Lean4

instance instZero : Zero (ModularForm Γ k) :=
  ⟨{  toSlashInvariantForm := 0
      holo' := fun _ => mdifferentiableAt_const
      bdd_at_cusps' hc g
        hg := by
        simp only [SlashInvariantForm.toFun_eq_coe, coe_zero, SlashAction.zero_slash]
        exact zero_form_isBoundedAtImInfty }⟩

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