vAdd_width_periodic — Mathlib

English

The slash-invariant form f is periodic of width N under horizontal translations by N·n along the vertical direction.

Русский

Форма SlashInvariantForm периодична по ширине N при горизонтальном переносе на N·n вдоль вертикали.

LaTeX

$$$ f(((N \\cdot n) \\mathbin{\\cdot} \\mathbb{R}) +_v z) = f(z) $$$

Lean4

theorem vAdd_width_periodic (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) :
    f (((N * n) : ℝ) +ᵥ z) = f z := by
  norm_cast
  rw [← modular_T_zpow_smul z (N * n), MulAction.compHom_smul_def, slash_action_eqn']
  · simp [-map_zpow, ModularGroup.coe_T_zpow (N * n)]
  · simpa using Subgroup.mem_map_of_mem (mapGL ℝ) <| ModularGroup_T_pow_mem_Gamma _ _ (Int.dvd_mul_right N n)

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