English
A similar product identity holds when h takes values in a multiplicative monoid and h is a homomorphism in each argument.
Русский
Аналогичное тождество произведения выполняется, когда h принимает значения в мультипликативном мономи, и является гомоморфизмом по каждому аргументу.
LaTeX
$$$$ (f+g).prod h = f.prod h \cdot g.prod h $$ при условии, что h(a) — гомоморфизм и выполняются соответствующие условия.$$
Lean4
@[simp]
theorem prod_hom_add_index [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} (h : α → Multiplicative M →* N) :
((f + g).prod fun a b => h a (Multiplicative.ofAdd b)) =
(f.prod fun a b => h a (Multiplicative.ofAdd b)) * g.prod fun a b => h a (Multiplicative.ofAdd b) :=
prod_add_index' (fun a => (h a).map_one) fun a => (h a).map_mul
