English
A specialized version: under simpler hypotheses, (f+g).prod h = f.prod h · g.prod h.
Русский
Специализированная версия: при более простых предпосылках, (f+g).prod h = f.prod h · g.prod h.
LaTeX
$$$$ (f+g).prod h = f.prod h \cdot g.prod h $$ под условием упрощения гипотез.$$
Lean4
/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
if `h` is an additive-to-multiplicative homomorphism.
This is a more specialized version of `Finsupp.prod_add_index` with simpler hypotheses. -/
@[to_additive /-- Taking the sum under `h` is an additive homomorphism of finsupps,if `h` is an additive
homomorphism. This is a more specific version of `Finsupp.sum_add_index` with simpler
hypotheses. -/
]
theorem prod_add_index' [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ a, h a 0 = 1)
(h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) : (f + g).prod h = f.prod h * g.prod h := by
classical exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a
