English
Let S be a finite index set and f : S → M. Then for a scalar a, a · E_{i∈S} f(i) = E_{i∈S} a · f(i).
Русский
Пусть S — конечный индексный набор, f:S→M. Тогда для скаляра a: a · E_{i∈S} f(i) = E_{i∈S} a · f(i).
LaTeX
$$$a \cdot \mathbb{E}_{i\in s} f(i) = \mathbb{E}_{i\in s} (a \cdot f(i)).$$$
Lean4
theorem expect_mul [IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a :=
by rw [expect, expect, smul_mul_assoc, sum_mul]