English
The scalar action of complex numbers is compatible with the graded multiplication on DirectSum ModularForm Γ.
Русский
Действие комплексных скаляров совместимо с градуированной умножением в DirectSum ModularForm Γ.
LaTeX
$$$\\alpha \\in \\mathbb{C},\\ f,g \\in \\bigoplus_k M_k(Γ)\\Rightarrow (\\alpha f)\\cdot g = \\alpha (f\\cdot g)$$$
Lean4
/-- Translating a `CuspForm` by `SL(2, ℤ)`, to obtain a new `CuspForm`. -/
noncomputable def translate [CuspFormClass F Γ k] (g : GL (Fin 2) ℝ) : CuspForm (toConjAct g⁻¹ • Γ) k
where
__ := ModularForm.translate f g
zero_at_cusps' {c} hc γ
hγ :=
by
rw [SlashInvariantForm.toFun_eq_coe, ModularForm.toSlashInvariantForm_coe, ModularForm.coe_translate, ←
SlashAction.slash_mul, ← isZeroAt_infty_iff, ← OnePoint.IsZeroAt.smul_iff]
apply CuspFormClass.zero_at_cusps f
simpa [mul_smul, hγ] using hc.smul g
