isSelfAdjoint

Mathlib.LinearAlgebra.Matrix.Hermitian

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

English

If A is Hermitian, then A is self-adjoint.

Русский

Если A эрмитова, то она самоприводима (self-adjoint).

LaTeX

$$A is Hermitian implies A is self-adjoint.$$

Lean4

protected theorem isSelfAdjoint {A : Matrix n n α} (h : A.IsHermitian) : IsSelfAdjoint A :=
  h

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

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

Разделы

Аффилиация

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