SL_slash — Mathlib

English

For γ ∈ SL(2,ℤ), the slash is compatible when converting from SL(2,ℤ) to GL(2,ℝ): (f ∣[k] γ) = (f ∣[k] (γ : GL(2,ℝ))).

Русский

Для γ ∈ SL(2,ℤ) слэш-операция согласуется при восприятии γ как элемента GL(2,ℝ): (f ∣[k] γ) = (f ∣[k] (γ : GL(2,ℝ))).

LaTeX

$$$ (f \lvert[k] \gamma) = (f \lvert[k] (\gamma : GL(2,\mathbb{R}))) $$$

Lean4

theorem SL_slash (γ : SL(2, ℤ)) : f ∣[k] γ = f ∣[k] (γ : GL (Fin 2) ℝ) :=
  rfl

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