submatrix_diagonal_embedding — Mathlib

English

For diagonal d and embedding e, the submatrix of diagonal d along e is the diagonal of d ∘ e.

Русский

Для диагонали d и вложения e подматрица диагонали d вдоль e равна диагонали d ∘ e.

LaTeX

$$$(\operatorname{diag} d)_{e,e} = \operatorname{diag}(d \circ e)$$$

Lean4

@[simp]
theorem submatrix_diagonal_embedding [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ↪ m) :
    (diagonal d).submatrix e e = diagonal (d ∘ e) :=
  submatrix_diagonal d e e.injective

Похожие утверждения