English
There is a canonical equivalence between matrices with I×J indexing of block entries and matrices whose rows and columns are indexed by I×K and J×L respectively, given by comp.
Русский
Существует каноническое соответствие между матрицами, чьи блоки индексируются парой индексов I×J, и матрицами, у которых строки и столбцы индексируются парой I×K и J×L соответственно, задаваемое через комп.
LaTeX
$$$ \mathrm{comp} : \mathrm{Matrix} I J (\mathrm{Matrix} K L R) \simeq \mathrm{Matrix} (I \times K) (J \times L) R $$$
Lean4
/-- I by J matrix where each entry is a K by L matrix is equivalent to
I × K by J × L matrix -/
@[simps]
def comp : Matrix I J (Matrix K L R) ≃ Matrix (I × K) (J × L) R
where
toFun m ik jl := m ik.1 jl.1 ik.2 jl.2
invFun n i j k l := n (i, k) (j, l)
