sum_smul_sum — Mathlib

English

For finite types α, β and functions f: α→R, g: β→M, the equality (sum over all α of f) smul (sum over all β of g) equals the double sum of f(i) smul g(j).

Русский

Для конечных множеств α, β и функций f: α→R, g: β→M: (∑i f(i)) • (∑j g(j)) = ∑i ∑j f(i) • g(j).

LaTeX

$$$$ \\left( \\sum_{i \\in \\mathrm{univ}} f(i) \\right) \\cdot \\left( \\sum_{j \\in \\mathrm{univ}} g(j) \\right) = \\sum_{i \\in \\mathrm{univ}} \\sum_{j \\in \\mathrm{univ}} f(i) \\cdot g(j). $$$$

Lean4

theorem sum_smul_sum [Fintype α] [Fintype β] (f : α → R) (g : β → M) : (∑ i, f i) • ∑ j, g j = ∑ i, ∑ j, f i • g j :=
  Finset.sum_smul_sum _ _

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