modular_T_smul — Mathlib

English

Special case of the T-action: T acts by translation by 1, so T · z = z + 1 for all z in the upper half-plane.

Русский

Особый случай действия T: T действует как сдвиг на 1, то есть T · z = z + 1 для всех z во верхней полуплоскости.

LaTeX

$$$T \cdot z = z + 1$$$

Lean4

theorem modular_T_smul (z : ℍ) : ModularGroup.T • z = (1 : ℝ) +ᵥ z := by
  simpa only [zpow_one, Int.cast_one] using modular_T_zpow_smul z 1

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