prod_sum_index — Mathlib

English

The product over a Finset of a sum of finsupps equals the sum of the products, componentwise.

Русский

Произведение над суммой финспп равно сумме произведений по компонентам.

LaTeX

$$$$ (\sum i \in s, g i).prod h = \prod i \in s (g i).prod h $$$$

Lean4

@[to_additive]
theorem prod_sum_index [Zero M] [AddCommMonoid N] [CommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P}
    (h_zero : ∀ a, h a 0 = 1) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (f.sum g).prod h = f.prod fun a b => (g a b).prod h :=
  (prod_finset_sum_index h_zero h_add).symm

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