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