modular_T_zpow_smul — Mathlib

English

For every z in the upper half-plane and every integer n, applying T^n to z translates z by n along the real axis: z ↦ z + n.

Русский

Для каждого z во верхней полуплоскости и каждого целого n применение T^n к z переводит z на величину n по действию по вещественной оси: z ↦ z + n.

LaTeX

$$$T^n \cdot z = z + n$$$

Lean4

theorem modular_T_zpow_smul (z : ℍ) (n : ℤ) : ModularGroup.T ^ n • z = (n : ℝ) +ᵥ z :=
  by
  rw [UpperHalfPlane.ext_iff, coe_vadd, add_comm, coe_specialLinearGroup_apply]
  simp [ModularGroup.coe_T_zpow, of_apply, cons_val_zero, Complex.ofReal_one, one_mul, cons_val_one, zero_mul, zero_add,
    div_one]

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