sum_smul_sum — Mathlib

English

For finite sets s ⊆ α and t ⊆ β, and functions f: α→R, g: β→M, the identity (sum i∈s f i) smul sum j∈t g j equals sum i∈s, sum j∈t f i smul g j.

Русский

Для конечных множеств s⊆α и t⊆β, функций f: α→R и g: β→M: (сумма по i∈s f(i)) умножает на сумму по j∈t g(j) равняется сумме по i∈s, j∈t f(i) умножить на g(j).

LaTeX

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

Lean4

theorem sum_smul_sum (s : Finset α) (t : Finset β) {f : α → R} {g : β → M} :
    (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j := by simp_rw [sum_smul, ← smul_sum]

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