sum_tmul — Mathlib

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]

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