diagonal_diag — Mathlib

English

A diagonal matrix is reconstructed by the diagonal of itself: diagonal (diag A) = A if A is diagonal.

Русский

Диагональная матрица восстанавливается по своей диагонали: diagonal (diag A) = A, если A диагональная.

LaTeX

$$$\text{diagonal}(\text{diag}(A)) = A \quad \text{whenever } A \text{ is diagonal.}$$$

Lean4

/-- Diagonal matrices are generated by the `Matrix.diagonal` of their `Matrix.diag`. -/
theorem diagonal_diag [Zero α] [DecidableEq n] {A : Matrix n n α} (h : A.IsDiag) : diagonal (diag A) = A :=
  ext fun i j => by
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [diagonal_apply_eq, diag]
    · rw [diagonal_apply_ne _ hij, h hij]

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