English
For a list l of elements in a Monoid α, noncommProd (l as multiset) comm equals l.prod, provided a suitable commutativity witness holds for the list elements.
Русский
Для списка l элементов моноида α некоммутативное произведение л -- это обычный произведение списка, если дано подходящее доказательство коммутативности для элементов списка.
LaTeX
$$$ (l:\\mathrm{List}\\ \\alpha).\\mathrm{noncommProd} \\ comm = l.prod $$$
Lean4
@[to_additive (attr := simp)]
theorem noncommProd_coe (l : List α) (comm) : noncommProd (l : Multiset α) comm = l.prod :=
by
rw [noncommProd]
simp only [noncommFold_coe]
induction l with
| nil => simp
| cons hd tl hl =>
rw [List.prod_cons, List.foldr, hl]
intro x hx y hy
exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)
