quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk

English

As above, but for the symmetric version on the right; the symm of prodRight sends (m1⊗m2, m1⊗m3) to m1 ⊗ (m2,m3).

Русский

Аналогично для симметричной версии справа: (prodRight)^{−1}(m1⊗m2, m1⊗m3) = m1 ⊗ (m2,m3).

LaTeX

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

Lean4

@[simp]
theorem quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk (m : Submodule R M) (n : Submodule R N) (x : M) (y : N) :
    quotientTensorQuotientEquiv m n (Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y) =
      Submodule.Quotient.mk (x ⊗ₜ y) :=
  rfl

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