kroneckerTMulLinearEquiv_tmul — Mathlib

English

There is an algebra isomorphism, over S, between the tensor product of two matrix algebras and the matrix algebra of the tensor product, compatible with the linear KR isomorphism.

Русский

Существует алгебраическое изоморфизм над S между тензорным произведением двух матричных алгебр и матричной алгеброй их тензорного произведения, совместимый с линейным изоморфизмом kroneckerTMul.

LaTeX

$$$ Matrix \; M_{m,m}(A) \otimes_R Matrix_{n,n}(B) \cong_S Matrix_{(m\times n),(m\times n)}(A \otimes_R B) $$$

Lean4

@[simp]
theorem kroneckerTMulLinearEquiv_tmul (a : Matrix l m M) (b : Matrix n p N) :
    kroneckerTMulLinearEquiv l m n p R S M N (a ⊗ₜ b) = a ⊗ₖₜ b :=
  rfl

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