prod_univ_fun_getElem — Mathlib

English

For any list l and any function f, the product over Fin(l.length) of f(l[i]) equals the product of the list mapped by f.

Русский

Для списка l и функции f произведение по i в Fin(l.length) f(l[i]) равно произведению списка l после отображения f.

LaTeX

$$$\displaystyle \prod_{i=\in \mathrm{Fin}(l.length)} f(l[i]) = \bigl(\mathrm{map}(f, l)\bigr).\mathrm{prod}$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_univ_fun_getElem (l : List ι) (f : ι → M) : ∏ i : Fin l.length, f l[i.1] = (l.map f).prod := by
  simp [Finset.prod_eq_multiset_prod]

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