English
For i ∈ ι₁, the symmetry of directSumLeft sends DirectSum.lof i (x ⊗ y) to the corresponding tensor factor x ⊗ DirectSum.lof i y.
Русский
Для i ∈ ι₁ симметрия directSumLeft отправляет DirectSum.lof i (x ⊗ y) в x ⊗ DirectSum.lof i y.
LaTeX
$$$$ (\\mathrm{TensorProduct.directSumLeft}\\, R\\, M_1\\, M_2').symm\\ (\\mathrm{DirectSum.lof}\\ R\\ ι_1\\ (fun i => M_1 i)\\ i\\ x \\otimes_R y) = \\mathrm{DirectSum.lof}\\ R\\ ι_1\\ (fun i => M_1 i)\\ i\\ (x) ⊗_R y. $$$$
Lean4
@[simp]
theorem directSumRight_tmul_lof (x : M₁') (i : ι₂) (y : M₂ i) :
directSumRight R M₁' M₂ (x ⊗ₜ[R] DirectSum.lof R _ _ i y) = DirectSum.lof R _ _ i (x ⊗ₜ[R] y) :=
by
dsimp only [directSumRight, LinearEquiv.trans_apply, TensorProduct.comm_tmul]
rw [directSumLeft_tmul_lof]
exact DFinsupp.mapRange_single (hf := fun _ => rfl)