English
For γ ∈ SL(2,ℤ), the slash at γ is given by (f ∣[k] γ)(τ) = f(γ · τ) denom(γ, τ)^{−k}.
Русский
Для γ ∈ SL(2,ℤ) slash-действие равно (f ∣[k] γ)(τ) = f(γ · τ) denom(γ, τ)^{−k}.
LaTeX
$$$ (f \lvert[k] γ)(τ) = f(γ \cdot τ) \; \mathrm{denom}(γ, τ)^{-k} $$$
Lean4
theorem mul_slash (k1 k2 : ℤ) (A : GL (Fin 2) ℝ) (f g : ℍ → ℂ) :
(f * g) ∣[k1 + k2] A = |(A.det : ℝ)| • (f ∣[k1] A * g ∣[k2] A) :=
by
ext1 x
simp only [slash_apply, Pi.mul_apply, Pi.smul_apply, real_smul, map_mul, neg_add, zpow_add₀ (denom_ne_zero _ x)]
set d := (↑|A.det.val| : ℂ)
have h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1) :=
by
have : d ≠ 0 := ofReal_ne_zero.mpr <| abs_ne_zero.mpr <| NeZero.ne _
rw [← zpow_one_add₀ this, ← zpow_add₀ this]
ring_nf
rw [h1]
ring
