prodRight_symm_tmul — Mathlib

English

The inverse of the ProdRight map sends a pair (m1⊗m2, m1⊗m3) back to m1 ⊗ (m2,m3).

Русский

Обратный отображатель ProdRight отправляет пару (m1⊗m2, m1⊗m3) обратно в m1 ⊗ (m2,m3).

LaTeX

$$$\\bigl(\\mathrm{prodRight}(R,S,M_1,M_2,M_3)\\bigr)^{-1}(m_1 \\otimes m_2,\\; m_1 \\otimes m_3) = m_1 \\otimes (m_2,m_3)$$$

Lean4

@[simp]
theorem prodRight_symm_tmul (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) :
    (prodRight R S M₁ M₂ M₃).symm (m₁ ⊗ₜ m₂, m₁ ⊗ₜ m₃) = (m₁ ⊗ₜ (m₂, m₃)) :=
  (LinearEquiv.symm_apply_eq _).mpr rfl

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