sum_mul_sum — Mathlib

English

Over completely finite index sets, the same double-sum identity holds: (∑ f i) (∑ g j) = ∑ i ∑ j f i g j.

Русский

Для полностью конечных множеств индексов верно тождество двойной суммы: (∑_i f_i)(∑_j g_j) = ∑_i ∑_j f_i g_j.

LaTeX

$$$$ (\\sum_{i} f(i)) (\\sum_{j} g(j)) = \\sum_{i} \\sum_{j} f(i) g(j). $$$$

Lean4

theorem sum_mul_sum (s : Finset ι) (t : Finset κ) (f : ι → R) (g : κ → R) :
    (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j := by simp_rw [sum_mul, ← mul_sum]

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