SLOnGLPos_smul_apply

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

English

The action respects multiplication on the left and right: (s • g) • z = ((s) * g) • z.

Русский

Действие сохраняет умножение слева и справа: (s • g) • z = ((s) * g) • z.

LaTeX

$$$(s \cdot g) \cdot z = (s g) \cdot z$$

Lean4

theorem SLOnGLPos_smul_apply (s : SL(2, ℤ)) (g : GL(2, ℝ)⁺) (z : ℍ) : (s • g) • z = ((s : GL(2, ℝ)⁺) * g) • z :=
  rfl

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

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

Разделы

Аффилиация

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