prodLeft_tmul — Mathlib

English

For elements m1 ∈ M1, m2 ∈ M2, m3 ∈ M3, the tmul on the left distributes as ((m1,m2) ⊗ m3) ↦ (m1 ⊗ m3, m2 ⊗ m3).

Русский

Для элементов m1 ∈ M1, m2 ∈ M2, m3 ∈ M3, применение tmul слева распадается так: ((m1,m2) ⊗ m3) ↦ (m1 ⊗ m3, m2 ⊗ m3).

LaTeX

$$$\\mathrm{prodLeft}(R,S,M_1,M_2,M_3)((m_1,m_2) \\otimes_\\mathrm{t} m_3) = (m_1 \\otimes_\\mathrm{t} m_3, \\; m_2 \\otimes_\\mathrm{t} m_3)$$$

Lean4

@[simp]
theorem prodLeft_tmul (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : prodLeft R S M₁ M₂ M₃ ((m₁, m₂) ⊗ₜ m₃) = (m₁ ⊗ₜ m₃, m₂ ⊗ₜ m₃) :=
  rfl

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