English
There is an algebra equivalence between matrices of block matrices and matrices with product-indexed blocks, respecting algebra structure, built from compRingEquiv.
Русский
Существет алгебраическое эквивалентное отображение между матрицами блочного вида и матрицами блоков, сохраняющее алгебраическую структуру, строимое через compRingEquiv.
LaTeX
$$$ \mathrm{compAlgEquiv} : \mathrm{Matrix} I I (\mathrm{Matrix} J J R) \simeq_{\mathsf{K}}^{\mathrm{Alg}} \mathrm{Matrix} (I \times J) (I \times J) R $$$
Lean4
/-- `Matrix.comp` as `AlgEquiv` -/
def compAlgEquiv : Matrix I I (Matrix J J R) ≃ₐ[K] Matrix (I × J) (I × J) R
where
__ := Matrix.compRingEquiv I J R
commutes' _ := comp_diagonal_diagonal _
