SL_neg_smul

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

English

Negating the matrix in SL(2, ℤ) does not change its action on the upper half-plane:

Русский

Умножение матрицы на −1 не меняет её действие на верхнюю полуплоскость.

LaTeX

$$$-g \cdot z = g \cdot z$$$

Lean4

@[simp high]
theorem SL_neg_smul : -g • z = g • z := by
  rw [sl_moeb, ← z.neg_smul]
  congr 1 with i j
  simp [toGL]

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

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

Разделы

Аффилиация

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