lTensorOne_tmul

Mathlib.LinearAlgebra.TensorProduct.Submodule

URI: https://scilib.ai/kg/mathlib#Submodule.lTensorOne_tmul

English

The symm of ProdLeft sends (m1⊗m3, m2⊗m3) to (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 lTensorOne_tmul (y : R) (n : N) : N.lTensorOne (algebraMap R _ y ⊗ₜ[R] n) = y • n :=
  N.lTensorOne'_tmul y n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru