prod_eq_multiset_prod — Mathlib

English

For any Finset s and function f: ι → M with M a commutative monoid, the Finset product equals the multiset product of mapped elements: ∏ x ∈ s, f x = (s.1.map f).prod.

Русский

Для любого Finset s и функции f: ι → M, где M — коммутативный моноид, произведение по элементам Finset равно произведению элементов мультисета, полученного отображением: ∏ x ∈ s, f x = (s.1.map f).prod.

LaTeX

$$$$ \\prod_{x \\in s} f(x) = (s.1.map f).prod $$$$

Lean4

@[to_additive]
theorem prod_eq_multiset_prod [CommMonoid M] (s : Finset ι) (f : ι → M) : ∏ x ∈ s, f x = (s.1.map f).prod :=
  rfl

Похожие утверждения