English
We can form a large matrix by stacking four blocks A, B, C, D into a big block matrix; fromBlocks(A,B,C,D) represents the matrix with A at top-left, B at top-right, C at bottom-left, and D at bottom-right.
Русский
Можно построить большую матрицу путём объединения четырёх блоков A, B, C, D: сверху слева A, сверху справа B, снизу слева C, снизу справа D.
LaTeX
$$\begin{pmatrix} A & B \\ C & D \end{pmatrix}$$
Lean4
/-- We can form a single large matrix by flattening smaller 'block' matrices of compatible
dimensions. -/
@[pp_nodot]
def fromBlocks (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) : Matrix (n ⊕ o) (l ⊕ m) α :=
of <| Sum.elim (fun i => Sum.elim (A i) (B i)) (fun j => Sum.elim (C j) (D j))
