modular_S_smul — Mathlib

English

Let z be a point in the upper half-plane. The S-element of the modular group acts on z by the Möbius transformation z ↦ -1/z.

Русский

Пусть z лежит во верхней полуплоскости. Элемент S модульной группы действует на z как преобразование Мёбиуса z ↦ -1/z.

LaTeX

$$$S \cdot z = -\dfrac{1}{z}$$$

Lean4

theorem modular_S_smul (z : ℍ) : ModularGroup.S • z = mk (-z : ℂ)⁻¹ z.im_inv_neg_coe_pos :=
  by
  rw [specialLinearGroup_apply]
  simp [ModularGroup.S, neg_div, inv_neg]

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