∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [inst : SMul α ℂ] [inst_1 : SMul α ℝ]
  [inst_2 : IsScalarTower α ℝ ℂ] (f : SlashInvariantForm Γ k) (n : α) (z : UpperHalfPlane), (n • f) z = n • f z