tensorTensorTensorComm_eq — Mathlib

English

Equality of two natural symmetry-related forms of tensorTensorTensorComm_symm_tmul across swapped inputs.

Русский

Равенство двух естественных форм симметрии tensorTensorTensorComm_symm_tmul для переставленных входов.

LaTeX

$$$\text{tensorTensorTensorComm}_{R S A B M N P Q}^{-1} = \text{tensorTensorTensorComm}_{R A S B M P N Q}$$$

Lean4

/-- The heterobasic version of `tensorTensorTensorComm` coincides with the regular version. -/
theorem tensorTensorTensorComm_eq :
    tensorTensorTensorComm R R R R M N P Q = TensorProduct.tensorTensorTensorComm R M N P Q :=
  rfl

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