English
Let M be a block matrix with blocks indexed by (i, k) and (j, k), and fix k ∈ o. The k-th diagonal block of M is the matrix whose (i, j)-entry is M((i, k), (j, k)).
Русский
Пусть M — блочная матрица с блоками, индексируемыми по парам (i, k) и (j, k). Тогда k-й диагональный блок M имеет элементы (i, j)-й пары: M((i, k), (j, k)).
LaTeX
$$$ (blockDiag M k)_{i j} = M_{(i,k),(j,k)} $$$
Lean4
/-- Extract a block from the diagonal of a block diagonal matrix.
This is the block form of `Matrix.diag`, and the left-inverse of `Matrix.blockDiagonal`. -/
def blockDiag (M : Matrix (m × o) (n × o) α) (k : o) : Matrix m n α :=
of fun i j =>
M (i, k)
(j, k)
-- TODO: set as an equation lemma for `blockDiag`, see https://github.com/leanprover-community/mathlib4/pull/3024
