English
Let M be a commutative monoid and S a submonoid of M. For any finite index set ι and any function f: ι → S, the finite product over i in a finite set s of f(i) equals the product in M of the same elements viewed in M.
Русский
Пусть M — коммутативный моноид, S — подмономод. Для любого конечного индексного множества ι и любой функции f: ι → S справедливо равенство произведений: произведение по i в ограниченном наборе s элементов f(i) равняется произведению тех же элементов, рассмотренных как элементы M.
LaTeX
$$$$ \\uparrow\\left(\\prod_{i \\in s} f(i)\\right) = \\prod_{i \\in s} (f(i) : M) $$$$
Lean4
@[to_additive (attr := norm_cast)]
theorem coe_finset_prod {ι M} [CommMonoid M] (S : Submonoid M) (f : ι → S) (s : Finset ι) :
↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : M) :=
map_prod S.subtype f s
