smul_sum — Mathlib

English

In a finite set, scalar multiplication distributes over the finite sum of a function f on γ: r • (∑_{x∈s} f x) = ∑_{x∈s} r • f x.

Русский

В конечном множестве скалярное умножение распределяется над конечной суммой функции: r • (∑_{x∈s} f(x)) = ∑_{x∈s} (r • f(x)).

LaTeX

$$$\\forall {\\gamma} {r:M} {s:\\mathsf{Finset} \\gamma} (f: \\gamma\\to N),\\; r \\cdot \\sum_{x\\in s} f(x) = \\sum_{x\\in s} r \\cdot f(x)$$$

Lean4

theorem smul_sum {f : γ → N} {s : Finset γ} : (r • ∑ x ∈ s, f x) = ∑ x ∈ s, r • f x :=
  map_sum (DistribSMul.toAddMonoidHom N r) f s

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