English
Let M be a matrix of matrices: M : Matrix m m (Matrix n n R). Then the square block of the composition corresponds to composing the square blocks with a relabeled indexing, i.e. there is an equality after reindexing that aligns the blocks with their positions.
Русский
Пусть M — матрица матриц: M : Matrix m m (Matrix n n R). Тогда квадратный блок композиции соответствует композиции квадратных блоков после переразметки индексов: существует равенство после перенумерации, согласующее блоки с их положениями.
LaTeX
$$$(M.comp\\ m\\ m\\ n\\ n\\ R)^{\\text{toSquareBlock}}_{(b,i)} = ((M^{\\text{toSquareBlock}}_{b,i}).\\text{comp} \\, \\dots)^{\\text{reindex}}$$$
Lean4
theorem comp_toSquareBlock {b : m → α} (M : Matrix m m (Matrix n n R)) (a : α) :
letI equiv := Equiv.prodSubtypeFstEquivSubtypeProd.symm
(M.comp m m n n R).toSquareBlock (fun i ↦ b i.1) a = ((M.toSquareBlock b a).comp _ _ n n R).reindex equiv equiv :=
rfl
