English
Let α1 and α2 be finite, M a commutative monoid, and f: α1 ⊕ α2 → M. Then the product over x of f x equals the product over a1 of f(Sum.inl a1) times the product over a2 of f(Sum.inr a2).
Русский
Пусть α1 и α2 конечны, M — коммутативный моноид, f: α1 ⊕ α2 → M. Тогда произведение по всем x от f x равно произведению по a1 от f(Sum.inl a1) умножить на произведение по a2 от f(Sum.inr a2).
LaTeX
$$$ \\displaystyle \\prod x, f x = \\left( \\prod a_1, f (\\mathrm{Sum}.inl a_1) \\right) \\cdot \\left( \\prod a_2, f (\\mathrm{Sum}.inr a_2) \\right). $$$
Lean4
@[to_additive (attr := simp)]
theorem prod_sum_type (f : α₁ ⊕ α₂ → M) : ∏ x, f x = (∏ a₁, f (Sum.inl a₁)) * ∏ a₂, f (Sum.inr a₂) :=
prod_disjSum _ _ _
