English
Let s be a finite set and f: α → β with β a Monoid. If the values f(x) commute pairwise for x ∈ s, then the noncommutative product over s of f equals the product of the f-values taken in a fixed order; in particular it is independent of the order.
Русский
Пусть s — конечное множество и f: α → β, где β — моноид. Если значения f(x) попарно коммутируют при x ∈ s, то некоммутативный произведение по s от f равняется произведению значений f в фиксированном порядке; следовательно, не зависит от порядка.
LaTeX
$$$ (s : \mathrm{Finset} \; \alpha) \; (f : \alpha \to \beta) \; (comm : (s : \mathrm{Set} \alpha).{\rm Pairwise} (\mathrm{Commute} \; on \; f)) \\Rightarrow \; \mathrm{noncommProd} \; s \; f \; comm = (\text{fixed order product of } f(a), a \in s)$$$
Lean4
/-- Product of a `s : Finset α` mapped with `f : α → β` with `[Monoid β]`,
given a proof that `*` commutes on all elements `f x` for `x ∈ s`. -/
@[to_additive /-- Sum of a `s : Finset α` mapped with `f : α → β` with `[AddMonoid β]`,
given a proof that `+` commutes on all elements `f x` for `x ∈ s`. -/
]
def noncommProd (s : Finset α) (f : α → β) (comm : (s : Set α).Pairwise (Commute on f)) : β :=
(s.1.map f).noncommProd <| noncommProd_lemma s f comm
