tmulEquiv_apply — Mathlib

English

The tmulEquiv maps a pair of tensor blocks to a single block indexed by a sum type.

Русский

tmulEquiv переводит пару тензорных блоков в один блок, индексированный суммой индексов.

LaTeX

$$$\\operatorname{tmulEquiv}_R M ((⨂ i, a_i) ⊗ (⨂ i, b_i)) = ⨂ i, \\mathrm{Sum.elim}(a,b) i$$$

Lean4

@[simp]
theorem tmulEquiv_apply (a : ι → M) (b : ι₂ → M) :
    tmulEquiv R M ((⨂ₜ[R] i, a i) ⊗ₜ[R] (⨂ₜ[R] i, b i)) = ⨂ₜ[R] i, Sum.elim a b i := by simp [tmulEquiv, Sum.elim]

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