IsHermitian — Mathlib

English

A matrix is Hermitian if it equals its conjugate transpose, i.e., A^H = A.

Русский

Матрица является эрмитовой тогда и только тогда, когда она равна своей сопряженной транспонированной: A^H = A.

LaTeX

$$$A^{\mathsf{H}} = A$$$

Lean4

/-- A matrix is Hermitian if it is equal to its conjugate transpose. On the reals, this definition
captures symmetric matrices. -/
def IsHermitian (A : Matrix n n α) : Prop :=
  Aᴴ = A

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