English
Tensor products distribute over a direct sum on the right: the isomorphism directSumRight maps x ⊗ DirectSum.lof i y to DirectSum.lof i (x ⊗ y).
Русский
Тензорные произведения распределяются по прямой сумме справа: прямой суммаRight отправляет x ⊗ DirectSum.lof i y в DirectSum.lof i (x ⊗ y).
LaTeX
$$$$ \\mathrm{directSumRight}\\, R\\, M_1'\\, M_2 \\bigl( x \\otimes_DirectSum.lof y \\bigr) = DirectSum.lof\\ R\\ ι_2\\ (x \\otimes y). $$$$
Lean4
@[simp]
theorem directSum_lof_tmul_lof (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
TensorProduct.directSum R S M₁ M₂ (DirectSum.lof S ι₁ M₁ i₁ m₁ ⊗ₜ DirectSum.lof R ι₂ M₂ i₂ m₂) =
DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂) :=
by simp [TensorProduct.directSum]