isZeroAt_iff_exists_SL2Z — Mathlib

English

Let c be a cusp and f: H → C, weight k. Then IsZeroAt c f k iff there exists γ ∈ SL(2,Z) with γ•∞ = c such that f|[k] γ vanishes at ∞.

Русский

Пусть c — cusp и f: H → C, вес k. Тогда IsZeroAt c f k эквивалентно существованию γ ∈ SL(2,Z) с γ•∞ = c, такого что f|[k] γ обращает нуль в ∞.

LaTeX

$$IsZeroAt(c,f,k) ↔ ∃ γ ∈ SL(2,Z), (γ•∞ = c) ∧ IsZeroAtImInfty (f|[k] γ)$$

Lean4

theorem isZeroAt_iff_exists_SL2Z (hc : IsCusp c 𝒮ℒ) :
    IsZeroAt c f k ↔ ∃ γ : SL(2, ℤ), mapGL ℝ γ • ∞ = c ∧ IsZeroAtImInfty (f ∣[k] γ) :=
  by
  constructor
  · obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
    simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using fun hfc ↦ ⟨γ, rfl, hfc⟩
  · rintro ⟨γ, rfl, b⟩
    simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using b

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