English
BlockDiagonal assembling a family of matrices M(k): matrix blocks M(k) along the diagonal of a large block matrix, with zeros elsewhere.
Русский
BlockDiagonal собирает семейство матриц M(k) вдоль диагонали большого блочного матричного объекта, остальные элементы — нули.
LaTeX
$$$\operatorname{blockDiagonal}(M) :\; (m \times o) \times (n \times o) \to \alpha$, где речь идёт о блок-матрице с блоками $M(k)$ на диагонали и нулями вне диагонали.$$
Lean4
/-- `Matrix.blockDiagonal M` turns a homogeneously-indexed collection of matrices
`M : o → Matrix m n α'` into an `m × o`-by-`n × o` block matrix which has the entries of `M` along
the diagonal and zero elsewhere.
See also `Matrix.blockDiagonal'` if the matrices may not have the same size everywhere.
-/
def blockDiagonal (M : o → Matrix m n α) : Matrix (m × o) (n × o) α :=
of <|
(fun ⟨i, k⟩ ⟨j, k'⟩ => if k = k' then M k i j else 0 : m × o → n × o → α)
-- TODO: set as an equation lemma for `blockDiagonal`, see https://github.com/leanprover-community/mathlib4/pull/3024
