slash_action_eqn — Mathlib

English

For any f, γ and hγ ∈ Γ, the image under the slash action equals the original function coerced to f.

Русский

Для любого f, γ и hγ ∈ Γ, значение slash-действия равно исходной функции, приведённой к f.

LaTeX

$$$\uparrow f \lvert[k] γ = \uparrow f$$$

Lean4

theorem slash_action_eqn [SlashInvariantFormClass F Γ k] (f : F) (γ) (hγ : γ ∈ Γ) : ↑f ∣[k] γ = ⇑f :=
  SlashInvariantFormClass.slash_action_eq f γ hγ

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