English
Modular forms carry a natural action of any scalar from the ambient scalar structure. For any c and f, the scalar multiple c · f is again a modular form of the same weight and level, and its values are obtained by pointwise scaling: (c · f)(z) = c · f(z) for all z in the upper half-plane.
Русский
Модульные формы имеют естественное скалярное действие над соответствующей скалярной структурой. Для любых c и f точно: c · f — это модульная форма того же веса и уровня, и значения задаются поканально как (c · f)(z) = c · f(z) для всех z из вещественной половины плоскости.
LaTeX
$$$ (c \cdot f)(z) = c \cdot f(z) \quad \text{for all } z \in \mathbb{H}. $$$
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
simpa only [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
SlashInvariantForm.coe_smulℝ, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash] using
(f.bdd_at_cusps' hc g hg).const_smul_left _ }
