English
A matrix M is diagonal with entries v if and only if its transpose is diagonal with the same entries: M^T = diagonal v ↔ M = diagonal v.
Русский
Матрица M является диагональной с данными значениями v тогда и только тогда, когда её транспонированная равна той же диагонали: M^T = diagonal(v) ↔ M = diagonal(v).
LaTeX
$$$M^\top = \mathrm{diagonal}(v) \;\Leftrightarrow\; M = \mathrm{diagonal}(v)$$$
Lean4
@[simp]
theorem transpose_eq_diagonal [DecidableEq n] [Zero α] {M : Matrix n n α} {v : n → α} :
Mᵀ = diagonal v ↔ M = diagonal v :=
(Function.Involutive.eq_iff transpose_transpose).trans <| by rw [diagonal_transpose]