rightComm_tmul — Mathlib

English

The heterobasic version of tensorTensorTensorComm coincides with the standard version; the two linear isomorphisms agree.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem rightComm_tmul (m : M) (p : P) (q : Q) : rightComm R S B M P Q ((m ⊗ₜ p) ⊗ₜ q) = (m ⊗ₜ q) ⊗ₜ p :=
  rfl

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