SL_slash_apply — Mathlib

English

For γ ∈ SL(2,ℤ), the slash of f at γ evaluated at τ is f(γ · τ) times denom(γ, τ)^{−k}.

Русский

Для γ ∈ SL(2,ℤ) значение (f ∣[k] γ)(τ) равно f(γ · τ) умножить на denom(γ, τ)^{−k}.

LaTeX

$$$ (f \lvert[k] γ)(τ) = f(γ \cdot τ) \; \text{denom}(γ, τ)^{-k} $$$

Lean4

theorem SL_slash_apply (γ : SL(2, ℤ)) (τ : ℍ) : (f ∣[k] γ) τ = f (γ • τ) * denom γ τ ^ (-k) := by
  simp [SL_slash, slash_def, σ]

Похожие утверждения