isDiag_iff_diagonal_diag — Mathlib

English

A IsDiag property holds for A if and only if diagonal (diag A) = A.

Русский

Свойство IsDiag выполняется для A тогда и только тогда, когда diagonal (diag A) = A.

LaTeX

$$$A.IsDiag \iff \ diagonal (diag A) = A.$$$

Lean4

/-- `Matrix.IsDiag.diagonal_diag` as an iff. -/
theorem isDiag_iff_diagonal_diag [Zero α] [DecidableEq n] (A : Matrix n n α) : A.IsDiag ↔ diagonal (diag A) = A :=
  ⟨IsDiag.diagonal_diag, fun hd => hd ▸ isDiag_diagonal (diag A)⟩

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