Hermitian matrices over ℝ and ℂ

This file proves that Hermitian matrices over ℝ and ℂ are exactly the ones whose corresponding linear map is self-adjoint.

Tags

self-adjoint matrix, hermitian matrix

theorem Matrix.IsHermitian.coe_re_apply_self {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] (h : A.IsHermitian) (i : n) : ↑(RCLike.re (A i i)) = A i i

The diagonal elements of a complex Hermitian matrix are real.

theorem Matrix.IsHermitian.coe_re_diag {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] (h : A.IsHermitian) : (fun (i : n) => ↑(RCLike.re (A.diag i))) = A.diag

The diagonal elements of a complex Hermitian matrix are real.

theorem Matrix.isHermitian_iff_isSymmetric {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] [Fintype n] [DecidableEq n] : A.IsHermitian ↔ (toEuclideanLin A).IsSymmetric

A matrix is Hermitian iff the corresponding linear map is self adjoint.

theorem Matrix.IsHermitian.im_star_dotProduct_mulVec_self {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] [Fintype n] (hA : A.IsHermitian) (x : n → 𝕜) : RCLike.im (star x ⬝ᵥ A.mulVec x) = 0