directSumRight_symm_lof_tmul — Mathlib

English

A variant of the previous lemma preserving the symmetry with tmul and lof interactions.

Русский

Вариант предыдущего лема, сохраняющий симметрию взаимодействий tmul и lof.

LaTeX

$$$$ (\\mathrm{TensorProduct.directSumLeft}\\, R\\, M_1\\, M_2').symm\\ (\\mathrm{DirectSum.lof}\\ R\\ ι_1\\ (fun i => M_1 i)\\ i\\ (x) ⊗_R y) = \\mathrm{DirectSum.lof}\\ R\\ ι_1\\ (fun i => M_1 i)\\ i\\ x ⊗_R y. $$$$

Lean4

@[simp]
theorem directSumRight_symm_lof_tmul (x : M₁') (i : ι₂) (y : M₂ i) :
    (directSumRight R M₁' M₂).symm (DirectSum.lof R _ _ i (x ⊗ₜ[R] y)) = x ⊗ₜ[R] DirectSum.lof R _ _ i y := by
  rw [LinearEquiv.symm_apply_eq, directSumRight_tmul_lof]

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