isHermitian_diagonal_iff — Mathlib

English

For any diagonal vector d, isHermitian if and only if every entry is self-adjoint (under a Star structure).

Русский

Для диагонального вектора d матрица диагональная эрмитова тогда и только тогда, когда каждый элемент self-adjoint.

LaTeX

$$[DecidableEq n] {d : n → α} : IsHermitian (diagonal d) ↔ (∀ i, IsSelfAdjoint (d i))$$

Lean4

/-- A diagonal matrix is Hermitian if each diagonal entry is self-adjoint -/
theorem isHermitian_diagonal_iff [DecidableEq n] {d : n → α} :
    IsHermitian (diagonal d) ↔ (∀ i : n, IsSelfAdjoint (d i)) := by
  simp [isSelfAdjoint_iff, IsHermitian, conjTranspose, diagonal_transpose, diagonal_map]

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