∀ {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ},
  3 ≤ k →
    ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ),
      UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k A ⇑(EisensteinSeries.eisensteinSeriesSIF a k))