prodRight_tmul — Mathlib

English

Under the right-distributive isomorphism, the tensor of a single element m1 with a pair (m2,m3) maps to the pair of tensors: m1 ⊗ (m2,m3) ↦ (m1⊗m2, m1⊗m3).

Русский

При правом распределении тензор на элемент m1 с парой (m2,m3) переходит в пару тензоров: m1⊗(m2,m3) ↦ (m1⊗m2, m1⊗m3).

LaTeX

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

Lean4

@[simp]
theorem prodRight_tmul (m₁ : M₁) (m : M₂ × M₃) : prodRight R S M₁ M₂ M₃ (m₁ ⊗ₜ m) = (m₁ ⊗ₜ m.1, m₁ ⊗ₜ m.2) :=
  rfl

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