golf

leanprover-community · May 3, 2023 · 51ed55e · 51ed55e
1 parent d1c29ed
commit 51ed55e
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/number_theory/modular_forms/slash_actions.lean b/src/number_theory/modular_forms/slash_actions.lean
@@ -98,6 +98,7 @@ def slash (k : ℤ) (γ : GL(2, ℝ)⁺) (f : ℍ → ℂ) (x : ℍ) : ℂ :=
 f (γ • x) * (((↑ₘ γ).det) : ℝ)^(k-1) * (upper_half_plane.denom γ x)^(-k)
 
 variables {Γ : subgroup SL(2, ℤ)} {k: ℤ} (f : ℍ → ℂ)
+
 section
 
 -- temporary notation until the instance is built