finset_prod_mk — Mathlib

English

The Finset version of the previous identity: the product over a Finset of mk(f i) equals mk of the product over i of f i.

Русский

Финсет-версия: произведение mk(f i) по i в p равно mk от произведения f i по i.

LaTeX

$$({p : Finset ι}) → (p.prod fun i => Associates.mk (f i)) = Associates.mk (p.prod fun i => f i)$$

Lean4

theorem finset_prod_mk {p : Finset ι} {f : ι → M} : (∏ i ∈ p, Associates.mk (f i)) = Associates.mk (∏ i ∈ p, f i) := by
  rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk, ← Finset.prod_eq_multiset_prod]

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