slash_action_eqn_SL'' — Mathlib

English

For slash-invariant forms of weight k with Γ a subgroup of SL(2, R), the same transformation law holds: f(γ · z) = (denom(γ, z))^k · f(z) for all γ ∈ Γ and z ∈ H.

Русский

Для слэш-инвариантных форм веса k при Γ ⊆ SL(2, R) выполняется то же преобразование: f(γ · z) = (denom(γ, z))^k · f(z) для всех γ ∈ Γ и z ∈ H.

LaTeX

$$$$ f(\\gamma \\cdot z) = (\\operatorname{denom}(\\gamma, z))^{k} f(z). $$$$

Lean4

/-- Every `SlashInvariantForm` `f` satisfies ` f (γ • z) = (denom γ z) ^ k * f z`. -/
theorem slash_action_eqn_SL'' {k : ℤ} {Γ : Subgroup SL(2, ℤ)} [SlashInvariantFormClass F Γ k] (f : F) {γ} (hγ : γ ∈ Γ)
    (z : ℍ) : f (γ • z) = (denom γ z) ^ k * f z :=
  SlashInvariantForm.slash_action_eqn' f (by simpa using hγ) z

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