English
Let M and N be commutative monoids and g: M →* N a monoid homomorphism. For any function f: α → M and any finite subset s ⊆ α, the homomorphism g preserves finite products, i.e. g(∏_{i ∈ s} f(i)) = ∏_{i ∈ s} g(f(i)).
Русский
Пусть M и N — коммутативные моноиды, g: M →* N — моноид-гомоморфизм. Для любой функции f: α → M и любой конечный набор s ⊆ α выполняется сохранение произведения: g(∏_{i ∈ s} f(i)) = ∏_{i ∈ s} g(f(i)).
LaTeX
$$$\operatorname{Finite}(s) \Rightarrow g\left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} g\bigl(f(i)\bigr)$$$
Lean4
/-- Given a monoid homomorphism `g : M →* N` and a function `f : α → M`, the value of `g` at the
product of `f i` over `i ∈ s` equals the product of `g (f i)` over `s`. -/
@[to_additive /-- Given an additive monoid homomorphism `g : M →* N` and a function `f : α → M`, the
value of `g` at the sum of `f i` over `i ∈ s` equals the sum of `g (f i)` over `s`. -/
]
theorem map_finprod_mem (f : α → M) (g : M →* N) (hs : s.Finite) : g (∏ᶠ j ∈ s, f j) = ∏ᶠ i ∈ s, g (f i) :=
g.map_finprod_mem' (hs.inter_of_left _)
