comm_trans_rTensorBot — Mathlib

English

Commutation on the right transfers to lTensorBot via equivalence.

Русский

Коммутирование справа переходит к lTensorBot через эквивалентность.

LaTeX

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

Lean4

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

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