English
A Finset product of (g i).prod h equals the product over the Finset of the sum (g i).prod h, given compatibility of h with addition.
Русский
Произведение по Finset равно произведению над суммой с учетом совместимости функций h.
LaTeX
$$$ \\prod\\limits_{i \\in s} (g i).prod h = (\\sum\\limits_{i \\in s} g i).prod h, $$$
Lean4
@[to_additive]
theorem prod_finset_sum_index {γ : Type w} {α : Type x} [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
[CommMonoid γ] {s : Finset α} {g : α → Π₀ 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₂) : (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h := by
classical
exact Finset.induction_on s (by simp [prod_zero_index]) (by simp +contextual [prod_add_index, h_zero, h_add])
