instSMulℂ — Mathlib

English

There is a scalar action of complex numbers on ModularForm Γ k compatible with the existing real/complex structures.

Русский

Существует скалярное действие комплексных чисел на ModularForm Γ k, совместимое с существующими реалиями и комплексной структурой.

LaTeX

$$$ (c \cdot f)(z) = c \cdot f(z) \quad \text{for all } z \in \mathbb{H}, \ c \in \mathbb{C}. $$$

Lean4

instance instSMulℂ : SMul α (ModularForm Γ k) where
  smul c
    f :=
    { toSlashInvariantForm := c • f.1
      holo' := by simpa using f.holo'.const_smul (c • (1 : ℂ))
      bdd_at_cusps' := fun hc g hg ↦
        by
        simp_rw [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
          SlashInvariantForm.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]
        exact (f.bdd_at_cusps' hc g hg).const_smul_left (σ g (c • (1 : ℂ))) }

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