glAction — Mathlib

English

There is a MulAction of GL(2,ℝ) on the upper half-plane ℍ extending the standard Möbius action, via the construction smulAux.

Русский

Существует действие MulAction GL(2,ℝ) на верхней полуплоскости ℍ, продолжающее стандартное преобразование Моебиуса через конструкцию smulAux.

LaTeX

$$$GL(2,\\\\mathbb{R}) \\\\text{ acts on } \\\\mathbb{H}, \\\\text{ via } g \\\\mapsto smulAux(g,\\\\cdot).$$$

Lean4

/-- Action of `GL (Fin 2) ℝ` on the upper half-plane, with `GL(2, ℝ)⁺` acting by Moebius
transformations in the usual way, extended to all of `GL (Fin 2) ℝ` using complex conjugation. -/
instance glAction : MulAction (GL (Fin 2) ℝ) ℍ where
  smul := smulAux
  one_smul
    z := by
    change smulAux 1 z = z
    simp [smulAux, smulAux', num, denom, σ]
  mul_smul := mul_smul'

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