comm_trans_lTensorBot — Mathlib

English

Commutation transformation transfers left tensor to right tensor, yielding equivalence with lTensorBot.

Русский

Преобразование коммутирования переносит левый тензор в правый, дав результат, эквивалентный lTensorBot.

LaTeX

$$$(\\mathrm{Algebra.TensorProduct.comm}\\ R\\ _\\ _).trans A.lTensorBot = A.rTensorBot$$$

Lean4

@[simp]
theorem comm_trans_lTensorBot : (Algebra.TensorProduct.comm R _ _).trans A.lTensorBot = A.rTensorBot :=
  AlgEquiv.toLinearEquiv_injective (toSubmodule A).comm_trans_lTensorOne

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