directSumRight_tmul_lof — Mathlib

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)

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