coe_mul — Mathlib

English

The function form of the product equals the product of the functions: (f.mul g) = f · g as functions.

Русский

Функциональное представление произведения равно произведению функций: (f.mul g) = f · g.

LaTeX

$$$\big(\,f.mul g\big) = f \cdot g\quad\text{as functions on } \mathbb{H}. $$$

Lean4

@[simp]
theorem coe_mul [Γ.HasDetPlusMinusOne] {k₁ k₂ : ℤ} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) :
    ⇑(f.mul g) = ⇑f * ⇑g :=
  rfl

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