English
Given a diagonal matrix diag(d) defined by d: m → α and a reindexing e: l → m that is injective, the submatrix obtained by restricting rows and columns via e is again diagonal, with diagonal d ∘ e.
Русский
Пусть diag(d) — диагональная матрица, заданная d: m → α, и e: l → m — инъекция. Подматрица, полученная ограничением по e, снова диагональная и имеет диагональ d ∘ e.
LaTeX
$$$\bigl(\operatorname{diag} d\bigr)_{e,e} = \operatorname{diag}(d \circ e).$$$
Lean4
/-- Given a `(m × m)` diagonal matrix defined by a map `d : m → α`, if the reindexing map `e` is
injective, then the resulting matrix is again diagonal. -/
theorem submatrix_diagonal [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l → m)
(he : Function.Injective e) : (diagonal d).submatrix e e = diagonal (d ∘ e) :=
ext fun i j => by
rw [submatrix_apply]
by_cases h : i = j
· rw [h, diagonal_apply_eq, diagonal_apply_eq, Function.comp_apply]
· rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]
