prod_univ_getElem — Mathlib

English

For any list l of elements of a commutative monoid M, the product over i in Fin(l.length) of l[i] equals the product of the list elements, i.e., l.prod.

Русский

Для любого списка l из элементов коммутативного моноида M произведение по i в Fin(l.length) l[i] равно произведению списка l.

LaTeX

$$$\displaystyle \prod_{i=\in \mathrm{Fin}(l.\text{length})} l[i] = \mathrm{prod}(l).$$$

Lean4

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

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