isHermitian_diagonal — Mathlib

English

A diagonal matrix is Hermitian if the entries have trivial star (e.g., on the reals).

Русский

Диагональная матрица эрмитова, если на её диагонали стоящие элементы — тривиальная операция звезды (например, на модулях вещественных чисел).

LaTeX

$$$[TrivialStar\ α] \Rightarrow (\text{diagonal } v)^{\mathsf{IsHermitian}}$$$

Lean4

/-- A diagonal matrix is Hermitian if the entries have the trivial `star` operation
(such as on the reals). -/
@[simp]
theorem isHermitian_diagonal [TrivialStar α] [DecidableEq n] (v : n → α) : (diagonal v).IsHermitian :=
  isHermitian_diagonal_of_self_adjoint _ (IsSelfAdjoint.all _)

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