tmulEquiv_symm_apply — Mathlib

English

The inverse of the tensor product reindexing maps back to the original split along Sum.inl and Sum.inr.

Русский

Обратное отображение тензорного произведения возвращает исходное разбиение по Sum.inl и Sum.inr.

LaTeX

$$$(\\mathrm{tmulEquiv})^{\\,-1}(⨂ i, a i) = (⨂ i, a(\\mathrm{Sum.inl}\, i)) \\otimes (⨂ i, a(\\mathrm{Sum.inr}\, i))$$$

Lean4

@[simp]
theorem tmulEquiv_symm_apply (a : ι ⊕ ι₂ → M) :
    (tmulEquiv R M).symm (⨂ₜ[R] i, a i) = (⨂ₜ[R] i, a (Sum.inl i)) ⊗ₜ[R] (⨂ₜ[R] i, a (Sum.inr i)) := by simp [tmulEquiv]

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