coe_finsuppProd — Mathlib

English

The coercion of the finsupp product equals the finsupp product of coerced terms.

Русский

Коэрцирование произведения finsupp равно произведению коэрцированных элементов.

LaTeX

$$$$ \\big( f . prod g \\big)^{\\uparrow} = f.prod (\\lambda i f_i, (g i f_i)^{\\uparrow}) $$$$

Lean4

@[to_additive]
theorem coe_finsuppProd [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) :
    ⇑(f.prod g) = f.prod fun i fi => ⇑(g i fi) :=
  MonoidHom.coe_finset_prod _ _

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