neg_smul

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.neg_smul

English

In the action on the upper half-plane, multiplying the matrix by −1 has no effect: −g acts the same as g on any z ∈ ℍ.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem neg_smul : -g • z = g • z := by
  ext1
  simp [coe_smul]

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

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

Разделы

Аффилиация

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