tensorTensorTensorComm_tmul — Mathlib

English

The tensor-tensor commutation morphism is symmetric in its arguments and respects the tower structure of the scalars.

Русский

Морфизм обмена тензорными компонентами симметричен по аргументам и сохраняет стек токенов скаляров.

LaTeX

$$tensorTensorTensorComm R R' S T A B C D = tensorTensorTensorComm R S R' T A C B D$$

Lean4

@[simp]
theorem tensorTensorTensorComm_tmul (m : A) (n : B) (p : C) (q : D) :
    tensorTensorTensorComm R R' S T A B C D (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ p ⊗ₜ (n ⊗ₜ q) :=
  rfl

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