submatrix_diagonal_equiv — Mathlib

English

If d: m → α and e: l ≃ m, then the diagonal of the submatrix equals the diagonal composed with e: (diagonal d).submatrix e e = diagonal (d ∘ e).

Русский

Пусть d: m → α и e: l ≃ m. Тогда диагональ подматрицы: (diagonal d).submatrix e e = diagonal (d ∘ e).

LaTeX

$$$(\operatorname{diagonal} d).submatrix e e = \operatorname{diagonal}(d \circ e)$$$

Lean4

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

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