∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ},
  IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range →
    (c.IsZeroAt f k ↔
      ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
        (Matrix.SpecialLinearGroup.mapGL ℝ) γ • OnePoint.infty = c →
          UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k γ f))