slash_action_eqn'' — Mathlib

English

Same transformation rule as above, for slash-invariant forms of weight k, but stated in terms of a slightly simplified expression: f(γ · z) = (denom(γ, z))^k · f(z) for all γ ∈ Γ and z ∈ H.

Русский

Та же формула преобразования для слэш-инвариантных форм весом k: f(γ · z) = (denom(γ, z))^k · f(z) для всех γ ∈ Γ и z ∈ верхняя полуплоскость.

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'' {k : ℤ} [Γ.HasDetOne] [SlashInvariantFormClass F Γ k] (f : F) {γ} (hγ : γ ∈ Γ) (z : ℍ) :
    f (γ • z) = (denom γ z) ^ k * f z :=
  SlashInvariantForm.slash_action_eqn' f hγ z

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