SLOnGLPos

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

URI: https://scilib.ai/kg/mathlib#ModularGroup.SLOnGLPos

English

The action of SL(2, ℤ) on GL(2, ℝ)⁺ sits inside as multiplication: s • g = s g.

Русский

Действие SL(2, ℤ) на GL⁺(2, ℝ) упорядочено как умножение: s • g = s g.

LaTeX

$$$s \cdot g = s g$$$

Lean4

instance SLOnGLPos : SMul SL(2, ℤ) GL(2, ℝ)⁺ :=
  ⟨fun s g => s * g⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru