English
There is a canonical linear isomorphism over S between the tensor product of two matrix algebras and the matrix algebra of the tensor product: Matrix l×m(M) ⊗ Matrix n×p(N) ≃ₗ[S] Matrix (l×n) (m×p) (M ⊗ N).
Русский
Существует каноническое линейное изоморфизмо над S между тензорным произведением двух матричных алгебр и матричной алгеброй тензорного произведения: Matrix l×m(M) ⊗ Matrix n×p(N) ≃ₗ[S] Matrix (l×n) (m×p) (M ⊗ N).
LaTeX
$$$ Matrix_{l,m}(M) \otimes_R Matrix_{n,p}(N) \cong_S Matrix_{(l\times n),(m\times p)}(M \otimes_R N) $$$
Lean4
/-- `Matrix.kroneckerTMul` as a linear equivalence, when the two arguments are tensored. -/
def kroneckerTMulLinearEquiv : Matrix l m M ⊗[R] Matrix n p N ≃ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N) :=
.ofLinear (AlgebraTensorModule.lift <| kroneckerTMulBilinear R S)
(Matrix.liftLinear R fun ii jj =>
AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2))
(by
ext : 4
simp [single_kroneckerTMul_single])
(by
ext : 5
simp [single_kroneckerTMul_single])
