transpose_eq_diagonal — Mathlib

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]

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