English
The tensor product distributes over finite sums in the first factor: m ⊗ (∑ a∈s n(a)) = ∑ a∈s (m ⊗ n(a)).
Русский
Тензорное произведение распределяется над суммой по первой компоненте: m ⊗ (∑_{a∈s} n(a)) = ∑_{a∈s} (m ⊗ n(a)).
LaTeX
$$$\\displaystyle m ⊗_R (\\sum_{a \\in s} n(a)) = \\sum_{a \\in s} (m ⊗_R n(a)).$$$
Lean4
theorem sum_tmul {α : Type*} (s : Finset α) (m : α → M) (n : N) : (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n := by
classical
induction s using Finset.induction with
| empty => simp
| insert _ _ has ih => simp [Finset.sum_insert has, add_tmul, ih]