SlashInvariantForm.slash_action_eqn

theorem SlashInvariantForm.slash_action_eqn : ∀ {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : SlashInvariantFormClass F Γ k] (f : F) (γ : ↥Γ), SlashAction.map ℂ k γ ⇑f = ⇑f

The theorem `SlashInvariantForm.slash_action_eqn` states that for all function-like objects `F` mapping from the upper half-plane to complex numbers, subgroup `Γ` of 2 by 2 special linear group over integers and integer `k`, if `F` has a class of slash invariant forms over `Γ` and `k`, then for any function `f` from `F` and any element `γ` from `Γ`, the slash action of `γ` on the function `f` is equal to the function `f` itself. This means the function `f` is invariant under the slash action.

More concisely: For function-like objects F mapping from the upper half-plane to complex numbers with a class of slash invariant forms over subgroup Γ of 2 by 2 special linear group over integers and integer k, the function f from F is invariant under the slash action of any element γ from Γ.