directSum_symm_lof_tmul — Mathlib

English

The equality directSumRight_tmul_lof asserts the expected behavior of directSumRight on tmul with lof.

Русский

Равенство directSumRight_tmul_lof описывает поведение directSumRight на tmul с lof.

LaTeX

$$$$ \\mathrm{directSumRight}\\, R\\, M_1'\\, M_2 \\ (x ⊗_R DirectSum.lof R\\, ι_2\\, M_2\\ i\\ y) = DirectSum.lof\\ R\\ ι_2\\ (x ⊗_R y). $$$$

Lean4

@[simp]
theorem directSum_symm_lof_tmul (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
    (TensorProduct.directSum R S M₁ M₂).symm
        (DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂)) =
      (DirectSum.lof S ι₁ M₁ i₁ m₁ ⊗ₜ DirectSum.lof R ι₂ M₂ i₂ m₂) :=
  by rw [LinearEquiv.symm_apply_eq, directSum_lof_tmul_lof]

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