prod_finset_sum_index — Mathlib

English

Product over i in a Finset s of (g i).prod h equals the product of the Finset sum (over i in s) of g i, each with h.

Русский

Произведение по i в конечном наборе s от (g i).prod h равно произведению суммы по i в s от g i, возведённого в h.

LaTeX

$$$$ \prod_{i \in s} (g(i)).prod h = (\sum_{i \in s} g(i)).prod h. $$$$

Lean4

@[to_additive]
theorem prod_finset_sum_index [AddCommMonoid M] [CommMonoid N] {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N}
    (h_zero : ∀ a, h a 0 = 1) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h :=
  Finset.cons_induction_on s rfl fun a s has ih => by rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]

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