mul'_comp_tensorTensorTensorComm — Mathlib

English

The two ways of multiplying inside a tensor product with two algebras are compatible: applying mul' on the tensor factors after tensorTensorTensorComm equals the tensor of the two mul' maps.

Русский

Две способы перемножения внутри тензорного произведения совместимы: применение mul' по каждой из компонент после tensorTensorTensorComm равно тензору mul' по обеим компонентам.

LaTeX

$$$\\operatorname{mul}'_R\\bigl(A\\otimes_R B\\bigr) \\circ (\\text{tensorTensorTensorComm } R\\; A\\; A\\; B\\; B) = \\text{map}(\\operatorname{mul}'_R A)\\bigl(\\operatorname{mul}'_R B\\bigr).$$$

Lean4

@[simp]
theorem mul'_comp_tensorTensorTensorComm :
    LinearMap.mul' R (A ⊗[R] B) ∘ₗ tensorTensorTensorComm R A A B B = map (LinearMap.mul' R A) (LinearMap.mul' R B) :=
  by
  ext
  simp

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