prod_sum — Mathlib

English

For a function f: ι → Multiset M and a Finset s, the product of the sums equals the product of the products: (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod.

Русский

Для функции f: ι → Multiset M и Finset s произведение суммы по x ∈ s от f x равно произведению произведений: (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod.

LaTeX

$$$$ \\left( \\sum_{x \\in s} f(x) \\right).prod = \\prod_{x \\in s} (f(x)).prod $$$$

Lean4

@[to_additive]
theorem prod_sum {ι : Type*} [CommMonoid M] (f : ι → Multiset M) (s : Finset ι) :
    (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod := by induction s using Finset.cons_induction with grind

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