From 51ed55eabec384120d410bfdf1b42f230e1deb7d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 3 May 2023 14:23:43 +0000 Subject: [PATCH] golf --- src/number_theory/modular_forms/slash_actions.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/number_theory/modular_forms/slash_actions.lean b/src/number_theory/modular_forms/slash_actions.lean index 2ac0b9eb44bdb..50bf0f5082445 100644 --- 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