English
The slash-invariant form product f.mul g has weight k1+k2 and is defined pointwise by (f.mul g)(τ) = f(τ) g(τ).
Русский
Произведение slash-инвариантной формы определяется как f.mul g с весом k1+k2 и значением на точке τ, равным f(τ) g(τ).
LaTeX
$$$\forall f:\mathrm{SlashInvariantForm}(\Gamma,k_1),\ g:\mathrm{SlashInvariantForm}(\Gamma,k_2),\ (f.mul g)(\tau) = f(\tau)\,g(\tau)\quad (\tau\in\mathbb{H}),\ k_1+k_2$ является весом форм.$$
Lean4
/-- The slash invariant form of weight `k₁ + k₂` given by the product of two slash-invariant forms
of weights `k₁` and `k₂`. -/
def mul [Γ.HasDetPlusMinusOne] {k₁ k₂ : ℤ} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) :
SlashInvariantForm Γ (k₁ + k₂) where
toFun := f * g
slash_action_eq' A
hA := by
simp [mul_slash, Subgroup.HasDetPlusMinusOne.abs_det hA, -Matrix.GeneralLinearGroup.val_det_apply,
slash_action_eqn f A hA, slash_action_eqn g A hA]
