English
The blockDiag of a diagonal matrix diagonal d is the diagonal matrix whose i-th diagonal entry is d(i,k).
Русский
Блочная диагональ диагональной матрицы diagonal d равна диагональной матрице с i-й диагональной записью d(i, k).
LaTeX
$$$ blockDiag (\mathrm{diagonal}(d))\,k = \mathrm{diagonal}(\lambda i. d(i,k)) $$$
Lean4
@[simp]
theorem blockDiag_diagonal [DecidableEq o] [DecidableEq m] (d : m × o → α) (k : o) :
blockDiag (diagonal d) k = diagonal fun i => d (i, k) :=
ext fun i j => by
obtain rfl | hij := Decidable.eq_or_ne i j
· rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]
· rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]
exact Prod.fst_eq_iff.mpr
