mul_sum — Mathlib

English

For any finite index sets I and K, the identity (∑ i f i) (∑ j g j) = ∑ i ∑ j f_i g_j holds.

Русский

Для любых конечных множеств индексов выполняется тождество (∑_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 mul_sum (s : Finset ι) (f : ι → R) (a : R) : a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i :=
  map_sum (AddMonoidHom.mulLeft a) _ s

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