sl_moeb — Mathlib

English

For g ∈ SL(2, ℤ) and z ∈ ℍ, the action of g on z equals the action of g regarded as GL(2, ℝ) on z; i.e., g • z = (g : GL(2, ℝ)) • z.

Русский

Для g ∈ SL(2, ℤ) и z ∈ ℍ действие g над z равно действию g, трактуемого как элемент GL(2, ℝ), над z; то есть g • z = (g : GL(2, ℝ)) • z.

LaTeX

$$$g \cdot z = (g : GL(2, \mathbb{R})) \cdot z$$$

Lean4

@[simp]
theorem sl_moeb : g • z = (g : GL (Fin 2) ℝ) • z :=
  rfl

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