English
If s and t are disjoint finite sets, then the noncommutative product over their union equals the product of the noncommutative products over each, with a commutation adjustment reflecting the partition.
Русский
Если s и t дискретны и не пересекаются, то некоммопрод по их объединению равен произведению некоммопродов по каждому из них, с учётом переноса коммутативности.
LaTeX
$$$ [DecidableEq \alpha] \; {s,t : \mathrm{Finset} \; \alpha} \; (h : \mathrm{Disjoint} \; s \; t) (f : \alpha \to \beta) (comm : {x | x \in s \cup t}.Pairwise (Commute on f)) : \\; noncommProd (s \cup t) f comm = \\; noncommProd s f (comm.mono <| coe_subset.2 subset_union_left) * \\; noncommProd t f (comm.mono <| coe_subset.2 subset_union_right)$$$
Lean4
@[to_additive]
theorem noncommProd_eq_prod {β : Type*} [CommMonoid β] (s : Finset α) (f : α → β) :
(noncommProd s f fun _ _ _ _ _ => Commute.all _ _) = s.prod f := by
induction s using Finset.cons_induction_on with
| empty => simp
| cons a s ha IH => simp [IH]
