tmul_sum — Mathlib

English

A pure tensor on the left distributes over a finite sum in the right argument: (m) ⊗ (∑ a∈s n(a)) = ∑ a∈s (m ⊗ n(a)).

Русский

Чистый тензор слева распределяется над суммой справа: m ⊗ (∑_{a∈s} n(a)) = ∑_{a∈s} (m ⊗ n(a)).

LaTeX

$$$ m ⊗_R (\\sum_{a \\in s} n(a)) = \\sum_{a \\in s} (m ⊗_R n(a)).$$$

Lean4

theorem tmul_sum (m : M) {α : Type*} (s : Finset α) (n : α → N) : (m ⊗ₜ[R] ∑ a ∈ s, n a) = ∑ a ∈ s, m ⊗ₜ[R] n a := by
  classical
    induction s using Finset.induction with
  | empty => simp
  | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]

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