prod_sumElim — Mathlib

English

Let α1, α2 finite, M a commutative monoid, f: α1 → M, g: α2 → M. Then the product over x in α1 ⊕ α2 of Sum.elim f g x equals the product over a1 of f a1 times the product over a2 of g a2.

Русский

Пусть α1, α2 конечны, M — коммутативный моноид, f: α1 → M, g: α2 → M. Тогда произведение по x из α1 ⊕ α2 от Sum.elim f g x равно произведению по a1 от f a1 и произведению по a2 от g a2.

LaTeX

$$$ \\displaystyle \\prod x, \\mathrm{Sum.elim} f g x = \\left( \\prod a_1, f a_1 \\right) \\cdot \\left( \\prod a_2, g a_2 \\right). $$$

Lean4

@[to_additive]
theorem prod_sumElim (f : α₁ → M) (g : α₂ → M) : ∏ x, Sum.elim f g x = (∏ a₁, f a₁) * ∏ a₂, g a₂ :=
  prod_disjSum _ _ _

Похожие утверждения