isHermitian_conjTranspose_iff

Mathlib.LinearAlgebra.Matrix.Hermitian

URI: https://scilib.ai/kg/mathlib#Matrix.isHermitian_conjTranspose_iff

English

IsHermitian is closed under conjTranspose equivalence: Aᴴ.IsHermitian ↔ A.IsHermitian.

Русский

Замыкание по сопряжённой транспонированной сохраняет эрмитовость: Aᴴ.IsHermitian ↔ A.IsHermitian.

LaTeX

$$$A^{\mathsf{H}}.IsHermitian \iff A.IsHermitian$$$

Lean4

@[simp]
theorem isHermitian_conjTranspose_iff (A : Matrix n n α) : Aᴴ.IsHermitian ↔ A.IsHermitian :=
  IsSelfAdjoint.star_iff

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

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

Разделы

Аффилиация

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