tensorμ_apply — Mathlib

English

On simple tensors, tensorμ acts as swapping the two pairs: tensorμ ((x ⊗ y) ⊗ (z ⊗ w)) = (x ⊗ z) ⊗ (y ⊗ w).

Русский

На простых тензорах tensorμ меняет пары местами: (x ⊗ y) ⊗ (z ⊗ w) ↦ (x ⊗ z) ⊗ (y ⊗ w).

LaTeX

$$$\\text{tensorμ } A B C D ((x \\otimes y) \\otimes (z \\otimes w)) = (x \\otimes z) \\otimes (y \\otimes w)$$$

Lean4

@[simp]
theorem tensorμ_apply {A B C D : ModuleCat R} (x : A) (y : B) (z : C) (w : D) :
    tensorμ A B C D ((x ⊗ₜ y) ⊗ₜ (z ⊗ₜ w)) = (x ⊗ₜ z) ⊗ₜ (y ⊗ₜ w) :=
  rfl

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