comm_trans_lTensorOne — Mathlib

English

The tensor product commutation transforms lTensorOne into rTensorOne, i.e., commutes with the left/right tensor isomorphisms.

Русский

Тождество перестановки тензорного произведения переводит lTensorOne в rTensorOne, т.е. коммутирует с соответствующими изоморфизмами.

LaTeX

$$$(\mathrm{TensorProduct}.\mathrm{comm} \ R \_ \_) \text{.trans } M.lTensorOne = M.rTensorOne$$$

Lean4

@[simp]
theorem comm_trans_lTensorOne : (TensorProduct.comm R _ _).trans M.lTensorOne = M.rTensorOne :=
  by
  refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun m r ↦ ?_
  obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2
  replace h : algebraMap R _ x = r := Subtype.val_injective h
  rw [← h]; simp

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