English
For a list l with pairwise distinct elements and a function f, the noncommutative product over the Finset l.toFinset equals the ordinary product of the list of f-values, provided the arguments commute as required.
Русский
Для списка l с попарно различными элементами и функции f некоммопрод по Finset l.toFinset равен обычному произведению значений f по списку, при соблюдении необходимых условий коммутативности.
LaTeX
$$$ [DecidableEq \alpha] \; (l : \mathrm{List} \; \alpha) \; (f : \alpha \to \beta) \; (comm) \; (hl : l.\mathrm{Nodup}) \\; noncommProd l.toFinset \; f \; comm = (l.map f).prod $$$
Lean4
@[to_additive (attr := simp)]
theorem noncommProd_toFinset [DecidableEq α] (l : List α) (f : α → β) (comm) (hl : l.Nodup) :
noncommProd l.toFinset f comm = (l.map f).prod :=
by
rw [← List.dedup_eq_self] at hl
simp [noncommProd, hl]
