English
Let {f_i} be a finite family of monoid homomorphisms f_i: M → N indexed by a finite set s. Then the product of these homomorphisms, evaluated at b ∈ M, equals the product of their evaluations at b:
Русский
Пусть дана конечная семейство гомоморфизмов f_i: M → N, индексируемое множеством s. Тогда произведение этих гомоморфизмов, применяемое к элементу b ∈ M, равно произведению значений на b:
LaTeX
$$$\\left(\\prod_{x \\in s} f_x\\right)(b) = \\prod_{x \\in s} f_x(b).$$$
Lean4
/-- See also `Finset.prod_apply`, with the same conclusion but with the weaker hypothesis
`f : α → M → N` -/
@[to_additive (attr := simp) /-- See also `Finset.sum_apply`, with the same conclusion but with the weaker hypothesis
`f : α → M → N` -/
]
theorem finset_prod_apply [MulOneClass M] [CommMonoid N] (f : ι → M →* N) (s : Finset ι) (b : M) :
(∏ x ∈ s, f x) b = ∏ x ∈ s, f x b :=
map_prod (MonoidHom.eval b) _ _
