isHermitian_diagonal_of_self_adjoint

English

A diagonal matrix diag(d) is Hermitian iff each diagonal entry d_i is self-adjoint.

Русский

Диагональная матрица diag(d) эрмитова тогда и только тогда, когда каждый диагональный элемент d_i самоприводим.

LaTeX

$$$\mathrm{IsHermitian}(\mathrm{diagonal}(d)) \iff \forall i, \mathrm{IsSelfAdjoint}(d_i)$$$

Lean4

/-- A diagonal matrix is Hermitian if the entries are self-adjoint (as a vector) -/
theorem isHermitian_diagonal_of_self_adjoint [DecidableEq n] (v : n → α) (h : IsSelfAdjoint v) :
    (diagonal v).IsHermitian :=
  (diagonal_conjTranspose v).trans <| congr_arg _ h

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