English
If d_i is a family of functions giving diagonal entries, then blockDiagonal' of the diagonal blocks equals a diagonal matrix whose entries come from d.
Русский
Если каждую диагональную часть задают функции d_i, то блочно-диагональная по диагоналям даёт диагональную матрицу с соответствующими элементами.
LaTeX
$$$ \\mathrm{blockDiagonal}' \\bigl( \\lambda k. \\mathrm{diagonal}(d k) \\bigr) = \\mathrm{diagonal} \\bigl( \\lambda \\langle i,j \\rangle. d\\, \\langle i,j \\rangle \\bigr) $$$
Lean4
@[simp]
theorem blockDiagonal'_diagonal [∀ i, DecidableEq (m' i)] (d : ∀ i, m' i → α) :
(blockDiagonal' fun k => diagonal (d k)) = diagonal fun ik => d ik.1 ik.2 :=
by
ext ⟨i, k⟩ ⟨j, k'⟩
simp only [blockDiagonal'_apply, diagonal]
obtain rfl | hij := Decidable.eq_or_ne i j
· simp
· simp [hij]
