prodLeft_symm_tmul — Mathlib

English

The inverse of the ProdLeft map sends ((m1,m2) ⊗ m3) back to (m1,m2) ⊗ m3; i.e., (prodLeft)^{-1}(m1⊗m3, m2⊗m3) = (m1,m2) ⊗ m3.

Русский

Обратное отображение ProdLeft отправляет (m1⊗m3, m2⊗m3) обратно в ((m1,m2) ⊗ m3).

LaTeX

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

Lean4

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

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