English
BlockDiag' applied to a diagonal matrix yields a diagonal matrix whose diagonal blocks come from the original diagonal data.
Русский
BlockDiag' применённая к диагональной матрице даёт диагональную матрицу с диагональными блоками, полученными из исходных данных.
LaTeX
$$$ \\mathrm{blockDiag}'( \\mathrm{diagonal}(d) ) k = \\mathrm{diagonal}( \\lambda i. d \\langle k,i \\rangle ) $$$
Lean4
@[simp]
theorem blockDiag'_diagonal [DecidableEq o] [∀ i, DecidableEq (m' i)] (d : (Σ i, m' i) → α) (k : o) :
blockDiag' (diagonal d) k = diagonal fun i => d ⟨k, i⟩ :=
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 (fun h => ?_) hij)]
cases h
rfl
