English
Let F be a space of slash-invariant forms of weight k for a subgroup Γ of GL2(R) with determinant one. Then for every f ∈ F, every γ ∈ Γ, and every z in the upper half-plane, the transformation rule holds: f(γ · z) = (denom(γ, z))^k · f(z).
Русский
Пусть F обозначает множество слэш-инвариантных форм весом k для подгруппы Γ ⊂ GL2(R) с определителем 1. Тогда для любого f ∈ F, любого γ ∈ Γ и любого z в верхней полуплоскости выполняется правило преобразования: f(γ · z) = (denom(γ, z))^k · f(z).
LaTeX
$$$$ f(\\gamma \\cdot z) = (\\operatorname{denom}(\\gamma, z))^{k} f(z). $$$$
Lean4
theorem slash_action_eqn' {k : ℤ} [Γ.HasDetOne] [SlashInvariantFormClass F Γ k] (f : F) {γ} (hγ : γ ∈ Γ) (z : ℍ) :
f (γ • z) = (γ 1 0 * z + γ 1 1) ^ k * f z :=
by
have : f (γ • z) = f z * denom γ z ^ k := by
simpa [slash_def, σ, mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ (denom_ne_zero _ _)),
Subgroup.HasDetOne.det_eq hγ] using congr_fun (slash_action_eqn f γ hγ) z
rw [this, denom, mul_comm]
