English
Let L be a finite sequence of indices ι, M and N be monoids, f: ι → M, and g be a monoid homomorphism from M to N. Then the product of g(f(i)) over i in L equals g applied to the product of f(i) over i in L: ∏_{i∈L} g(f(i)) = g(∏_{i∈L} f(i)).
Русский
Пусть L — конечная последовательность индексов ι, моноиды M и N; функция f:ι → M и моноидный гомоморфизм g: M → N. Тогда произведение g(f(i)) по всем i из L равно g применённому к произведению f(i) по i из L: ∏_{i∈L} g(f(i)) = g(∏_{i∈L} f(i)).
LaTeX
$$$ (L.map (g \circ f)).prod = g \bigl((L.map f).prod\bigr) $$$
Lean4
@[to_additive]
theorem prod_map_hom (L : List ι) (f : ι → M) {G : Type*} [FunLike G M N] [MonoidHomClass G M N] (g : G) :
(L.map (g ∘ f)).prod = g (L.map f).prod := by rw [← prod_hom, map_map]
