English
There is an explicit identity for the blockDiagonal' structure when indexing over o; in particular, blockDiagonal' with one-dimensional blocks yields a standard block matrix identity.
Русский
Существуют явные единичные выражения для структуры blockDiagonal' по индексации по o; в частности, блоки размерности единицы дают стандартную единичную матрицу блоков.
LaTeX
$$$ \\mathrm{blockDiagonal'}(1) = 1 $$$
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 (Σ i, m' i) (Σ i, n' i) α) (k : o) : Matrix (m' k) (n' k) α :=
of fun i j =>
M ⟨k, i⟩
⟨k, j⟩
-- TODO: set as an equation lemma for `blockDiag'`, see https://github.com/leanprover-community/mathlib4/pull/3024
