isHermitian

Mathlib.LinearAlgebra.Matrix.PosDef

URI: https://scilib.ai/kg/mathlib#Matrix.PosSemidef.isHermitian

English

If a matrix M is positive semidefinite, then M is Hermitian.

Русский

Если матрица M положительно полуопределена, то она эрмитова.

LaTeX

$$$\text{PosSemidef}(M) \Rightarrow M \text{Is Hermitian}$$$

Lean4

theorem isHermitian {M : Matrix n n R} (hM : M.PosSemidef) : M.IsHermitian :=
  hM.1

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

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

Разделы

Аффилиация

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