English
General equality: for finsupp-valued objects f, g, h, the product of sums equals the sum of products across indices.
Русский
Общее равенство: произведение сумм равно сумме произведений по индексам.
LaTeX
$$$ (\\prod i \\; f_i) \\;\\bigl( h(i) \\bigr) = \\prod i \\; (f_i \\cdot h(i)). $$$
Lean4
@[to_additive]
theorem prod_sum_index {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
[∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
{f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} {h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1)
(h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) : (f.sum g).prod h = f.prod fun i b => (g i b).prod h :=
(prod_finset_sum_index h_zero h_add).symm
