instSMul — Mathlib

English

There is a scalar action of a type α on SlashInvariantForm Γ k, compatible with the slash action; for c ∈ α and f ∈ SlashInvariantForm Γ k, (c • f)(z) = c • f(z).

Русский

Существует скалярное действие над SlashInvariantForm Γ k от типа α, совместимое со слэш-акцией: (c • f)(z) = c • f(z).

LaTeX

$$$$ (c \\cdot f)(z) = c \\cdot f(z) \\quad (z \\in \\mathbb{H}). $$$$

Lean4

/-- Scalar multiplication by `ℂ`, assuming that `Γ ⊆ SL(2, ℝ)`. -/
instance instSMul : SMul α (SlashInvariantForm Γ k) where
  smul c
    f :=
    { toFun := c • ↑f
      slash_action_eq' γ
        hγ := by
        rw [← smul_one_smul ℂ]
        simp [-smul_assoc, smul_slash, slash_action_eqn _ _ hγ, σ, Subgroup.HasDetOne.det_eq hγ] }

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