sum_mul_sum — Mathlib

English

A restatement asserting the same double-sum identity in a particular naming convention.

Русский

Повторение той же двойной суммы в другой нотации.

LaTeX

$$$$ \\text{sum_mul_sum}_{\\mathrm{Fintype}}(f,g) : (\\sum_i f(i)) \\cdot \\sum_j g(j) = \\sum_i \\sum_j f(i) g(j). $$$$

Lean4

theorem _root_.Fintype.sum_mul_sum [Fintype ι] [Fintype κ] (f : ι → R) (g : κ → R) :
    (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j :=
  Finset.sum_mul_sum _ _ _ _

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