English
Let a be a congruence parameter and γ ∈ SL(2,Z). The weight-k Eisenstein series transforms under the SL(2,Z) action by the slash operator in a precise way: the transformed series with parameter a is obtained by applying γ to the parameter and keeping the weight fixed.
Русский
Пусть параметр конгруэнции a и γ ∈ SL(2, Z). Ряд Эйзенштейна веса k трансформируется по действию SL(2, Z) через операцию slash: преобразованный по γ ряд с параметром a получается заменой параметра на a⋅γ и сохранением веса.
LaTeX
$$$\mathrm{eisensteinSeries}\_{{a}}(k) \big|\!\!\_{{k}} \gamma = \mathrm{eisensteinSeries}\_{{a\,\vcenter{\ensuremath{\ast}}}\gamma}(k).$$$
Lean4
theorem eisensteinSeries_slash_apply (k : ℤ) (γ : SL(2, ℤ)) :
eisensteinSeries a k ∣[k] γ = eisensteinSeries (a ᵥ* γ) k :=
by
ext1 z
simp_rw [SL_slash_apply, zpow_neg, mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ <| denom_ne_zero _ z), eisensteinSeries,
eisSummand_SL2_apply, tsum_mul_left, mul_comm (_ ^ k)]
congr 1
exact (gammaSetEquiv a γ).tsum_eq (eisSummand k · z)
