kroneckerTMulAlgEquiv — Mathlib

English

The algebraic isomorphism matrixEquivTensor provides an equivalence between A ⊗_R Matrix n n R and Matrix n n A.

Русский

Алгебраическое тождество matrixEquivTensor устанавливает эквивалентность между A ⊗_R Matrix n n R и Matrix n n A.

LaTeX

$$$ matrixEquivTensor : A \otimes_R Matrix\,n\,n\,R \cong Matrix\,n\,n\,A $$$

Lean4

/-- `Matrix.kroneckerTMul` as an algebra equivalence, when the two arguments are tensored. -/
def kroneckerTMulAlgEquiv : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B) :=
  .ofLinearEquiv (kroneckerTMulLinearEquiv m m n n R S A B) (kroneckerTMulLinearEquiv_one _ _ _ _ _)
    (kroneckerTMulLinearEquiv_mul _ _ _ _ _)

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