∀ (k : ℤ) (γ : GL (Fin 2) ℝ) (f : UpperHalfPlane → ℂ) (x : UpperHalfPlane),
  ModularForm.privateSlash✝ k γ f x =
    (UpperHalfPlane.σ γ) (f (γ • x)) * ↑|↑(Matrix.GeneralLinearGroup.det γ)| ^ (k - 1) *
      UpperHalfPlane.denom γ ↑x ^ (-k)