rightComm_eq — Mathlib

English

The heterobasic tensorTensorTensorComm equals the standard one; the two expressions coincide as linear isomorphisms.

Русский

Гетеробазовая tensorTensorTensorComm равна стандартной; две конструкции совпадают как линейные изоморфизмы.

LaTeX

$$$\text{tensorTensorTensorComm}_{R S A B M N P Q} = \text{TensorProduct.tensorTensorTensorComm}_{R M N P Q}$$$

Lean4

/-- The heterobasic version of `leftComm` coincides with the regular version. -/
theorem rightComm_eq [Module R P] : rightComm R R R M P Q = TensorProduct.rightComm R M P Q :=
  rfl

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