English
For a function f: ι → M and a list l with no duplicates, the product over l.toFinset of f equals the product of the list mapped by f: (l.toFinset).prod f = (l.map f).prod.
Русский
Для функции f: ι → M и списка l без повторов произведение по l.toFinset от f равно произведению списка, полученного применением f ко всем элементам списка: (l.toFinset).prod f = (l.map f).prod.
LaTeX
$$$$ (l.toFinset).prod\\, f = (l.map\\, f).prod $$$$
Lean4
@[to_additive]
theorem prod_toFinset {M : Type*} [DecidableEq ι] [CommMonoid M] (f : ι → M) :
∀ {l : List ι} (_hl : l.Nodup), l.toFinset.prod f = (l.map f).prod
| [], _ => by simp
| a :: l, hl => by
let ⟨notMem, hl⟩ := List.nodup_cons.mp hl
simp [Finset.prod_insert (mt List.mem_toFinset.mp notMem), prod_toFinset _ hl]
