English
The product of two modular forms f and g of weights k1 and k2 is a modular form of weight k1 + k2; its value is the product of the values: (f.mul g)(z) = f(z) g(z).
Русский
Произведение двух модульных форм f и g весов k1 и k2 является модульной формой веса k1 + k2; значение равно произведению значений: (f.mul g)(z) = f(z) g(z).
LaTeX
$$$ (f \cdot g)(z) = f(z) \cdot g(z) \quad \text{and} \quad \text{weight}(f.m? g) = k_1 + k_2. $$$
Lean4
/-- The modular form of weight `k_1 + k_2` given by the product of two modular forms of weights
`k_1` and `k_2`. -/
def mul {k_1 k_2 : ℤ} [Γ.HasDetPlusMinusOne] (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) : ModularForm Γ (k_1 + k_2)
where
toSlashInvariantForm := f.1.mul g.1
holo' := f.holo'.mul g.holo'
bdd_at_cusps' hc γ hγ := by simpa [mul_slash] using ((f.bdd_at_cusps' hc γ hγ).mul (g.bdd_at_cusps' hc γ hγ)).smul _
