coe_re_diag

Mathlib.LinearAlgebra.Matrix.Hermitian

URI: https://scilib.ai/kg/mathlib#Matrix.IsHermitian.coe_re_diag

← MathLib Explorer

English

If A is Hermitian, then A^{-1} is Hermitian.

Русский

Если A Гермитова, то A^{-1} Гермитова.

LaTeX

$$(A^{-1})^{\\ast} = A^{-1}$$

Lean4

/-- The diagonal elements of a complex Hermitian matrix are real. -/
theorem coe_re_diag {A : Matrix n n α} (h : A.IsHermitian) : (fun i => (re (A.diag i) : α)) = A.diag :=
  funext h.coe_re_apply_self

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru