English
For any Finset s and function f: ι → M, the product over mapped elements equals the mapped product over the Finset: (s.1.map f).prod = ∏ a ∈ s, f a.
Русский
Для любого Finset s и функции f: ι → M произведение отображённых элементов равно отображённому произведению по элементам Finset: (s.1.map f).prod = ∏ a ∈ s, f a.
LaTeX
$$$$ (s.1).prod = \\prod_{a \\in s} f(a) $$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_map_val [CommMonoid M] (s : Finset ι) (f : ι → M) : (s.1.map f).prod = ∏ a ∈ s, f a :=
rfl