T_zpow_width_invariant — Mathlib

English

Applying T^(N n) to z yields the same value of f as z itself, i.e., width-invariance under T-zpow actions.

Русский

Применение T^(N n) к z даёт такое же значение f, как и к самому z; инвариантность по ширине T-зоw.

LaTeX

$$$ f\\bigl((\\mathrm{ModularGroup}.T)^{(N \\cdot n)} \\cdot z\\bigr) = f(z) $$$

Lean4

theorem T_zpow_width_invariant (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) :
    f (((ModularGroup.T ^ (N * n))) • z) = f z :=
  by
  rw [modular_T_zpow_smul z (N * n)]
  simpa only [Int.cast_mul, Int.cast_natCast] using vAdd_width_periodic N k n f z

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