∀ (k : ℤ) (f f' : UpperHalfPlane → ℂ) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane),
  UpperHalfPlane.petersson k f f' (g • τ) =
    UpperHalfPlane.petersson k (SlashAction.map k g f) (SlashAction.map k g f') τ