coe_T_zpow_smul_eq — Mathlib

English

For any integer n, the action of T^n on z shifts the complex number by n: (T^n • z) = z + n.

Русский

Для любого целого n действие T^n на z сдвигает комплексную координату на n: T^n•z = z + n.

LaTeX

$$$\\forall n\\in \\mathbb{Z},\\; (T^n\\cdot z) = z + n.$$$

Lean4

theorem coe_T_zpow_smul_eq {n : ℤ} : (↑(T ^ n • z) : ℂ) = z + n :=
  by
  rw [UpperHalfPlane.coe_specialLinearGroup_apply]
  simp [coe_T_zpow, -map_zpow]

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