Finsupp.coe_mul

theorem Finsupp.coe_mul : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂

The theorem `Finsupp.coe_mul` states that for any two functions `g₁` and `g₂` from an arbitrary type α to another type β (where β is a multiplication class that contains zero), the process of applying a function to the product of `g₁` and `g₂` (represented by `⇑(g₁ * g₂)`) is equivalent to the product of the results of applying the function to `g₁` and `g₂` separately (represented by `⇑g₁ * ⇑g₂`).

More concisely: For any functions `g₁` and `g₂` from type `α` to a multiplication class `β` with zero, `⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂`.