prod_map_val — Mathlib

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

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