Finset.smul_sum

theorem Finset.smul_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid β] [inst_1 : DistribSMul α β] {r : α} {f : γ → β} {s : Finset γ}, (r • s.sum fun x => f x) = s.sum fun x => r • f x

The theorem `Finset.smul_sum` states that for all types `α`, `β`, `γ`, under the condition that `β` is an additive commutative monoid and `α` and `β` together form a distributive scalar multiplication system, for any scalar `r` of type `α`, any function `f` from `γ` to `β`, and any finite set `s` of elements of type `γ`, the scalar multiplication of `r` and the sum of `f(x)` for each `x` in `s` is equal to the sum of `r • f(x)` for each `x` in `s`. In other words, it asserts that scalar multiplication distributes over the summation operation in a finite set, a property analogous to the distributive law in algebra: $r \cdot \sum_{x \in S} f(x) = \sum_{x \in S} r \cdot f(x)$, where $S$ is a finite set, $r$ is a scalar, and $f(x)$ is a function mapping elements of the set to the monoid.

More concisely: For any scalar `r`, additive commutative monoid `β`, distributive scalar multiplication system `α` and `β`, and finite set `s` of elements `γ`, the scalar multiplication of `r` and the sum of `f(x)` for each `x` in `s` equals the sum of `r • f(x)` for each `x` in `s`.