sum_mul — Mathlib

English

The product of the sums equals the double sum of pairwise products: (∑ f i) (∑ g j) = ∑_i ∑_j f_i g_j.

Русский

Произведение сумм равно двойному суммированию по парам: (∑_i f_i) (∑_j g_j) = ∑_i ∑_j f_i g_j.

LaTeX

$$$$ \\Big( \\sum_{i \\in s} f(i) \\Big) \\cdot \\Big( \\sum_{j \\in t} g(j) \\Big) = \\sum_{i \\in s} \\sum_{j \\in t} f(i) \\cdot g(j). $$$$

Lean4

theorem sum_mul (s : Finset ι) (f : ι → R) (a : R) : (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a :=
  map_sum (AddMonoidHom.mulRight a) _ s

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