instAdd — Mathlib

English

Let Γ ≤ SL(2, R). For all f ∈ SlashInvariantForm Γ k and γ ∈ Γ, z ∈ H, f(γ · z) = (denom γ z)^k f(z).

Русский

Пусть Γ ⊆ SL(2, R). Для всех f ∈ SlashInvariantForm Γ k и γ ∈ Γ, z ∈ H выполняется f(γ · z) = (denom γ z)^k f(z).

LaTeX

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

Lean4

instance instAdd : Add (SlashInvariantForm Γ k) :=
  ⟨fun f g ↦
    { toFun := f + g
      slash_action_eq' := fun γ hγ ↦ by rw [SlashAction.add_slash, slash_action_eqn f γ hγ, slash_action_eqn g γ hγ] }⟩

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