English
Given a multiset s of elements in a Monoid α and a proof that the elements commute pairwise, the noncommutative product noncommProd(s, comm) is defined by folding with multiplication and unit 1: noncommProd(s, comm) = s.noncommFold (· ·) comm 1.
Русский
Пусть s — мультиcет элементов в моноиде α, и существует доказательство попарной совместимости элементов; тогда определено некоммутативное произведение: noncommProd(s, comm) = s.noncommFold(··) comm 1.
LaTeX
$$$\\mathrm{noncommProd}(s, comm) = s.\\mathrm{noncommFold}(\\cdot \\ast \\cdot)\\; comm\\; 1$.$$
Lean4
theorem noncommFold_cons (s : Multiset α) (a : α) (h h') (x : α) :
noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x) :=
by
induction s using Quotient.inductionOn
simp
