English
If H is a family of monoid homs, then applying H to a product over a DFinsupp equals the product over the mapped arguments.
Русский
Если H — семейство однородных гомоморфизмов, то применение H к произведению над DFinsupp равно произведению, полученному применением H к соответствующим аргументам.
LaTeX
$$$ h( f.prod g ) = f.prod (\\lambda a b . h( g(a,b) )) $$$
Lean4
@[to_additive (attr := simp)]
theorem _root_.map_dfinsuppProd {R S H : Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid R]
[CommMonoid S] [FunLike H R S] [MonoidHomClass H R S] (h : H) (f : Π₀ i, β i) (g : ∀ i, β i → R) :
h (f.prod g) = f.prod fun a b => h (g a b) :=
map_prod _ _ _
