English
BlockDiagonal' turns a family of matrices indexed by o into a block matrix indexed by Σ o, mapping diagonal blocks to M k i j and off-diagonals to zero.
Русский
BlockDiagonal' превращает семейство матриц в блочную матрицу; на диагонали располагаются M k i j, остальное ноль.
LaTeX
$$$ blockDiagonal' (M) ⟨k,i⟩ ⟨k',j⟩ = \text{if } h: k = k' \text{ then } M k i (cast (congr_arg n' h.symm) j) \text{ else } 0 $$$
Lean4
/-- `Matrix.blockDiagonal' M` turns `M : Π i, Matrix (m i) (n i) α` into a
`Σ i, m i`-by-`Σ i, n i` block matrix which has the entries of `M` along the diagonal
and zero elsewhere.
This is the dependently-typed version of `Matrix.blockDiagonal`. -/
def blockDiagonal' (M : ∀ i, Matrix (m' i) (n' i) α) : Matrix (Σ i, m' i) (Σ i, n' i) α :=
of <|
(fun ⟨k, i⟩ ⟨k', j⟩ => if h : k = k' then M k i (cast (congr_arg n' h.symm) j) else 0 :
(Σ i, m' i) → (Σ i, n' i) → α)
-- TODO: set as an equation lemma for `blockDiagonal'`, see https://github.com/leanprover-community/mathlib4/pull/3024
