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)
:
The diagonal elements of a complex Hermitian matrix are real.
@[simp]
theorem
Matrix.isSymmetric_toLin_iff
{𝕜 : Type u_1}
{n : Type u_3}
{A : Matrix n n 𝕜}
[RCLike 𝕜]
[Fintype n]
[DecidableEq n]
{E : Type u_4}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(b : OrthonormalBasis n 𝕜 E)
:
A matrix is Hermitian iff the corresponding linear map with an orthonormal basis is symmetric.
@[simp]
theorem
Matrix.isSymmetric_toEuclideanLin_iff
{𝕜 : Type u_1}
{n : Type u_3}
{A : Matrix n n 𝕜}
[RCLike 𝕜]
[Fintype n]
[DecidableEq n]
:
A matrix is Hermitian iff the corresponding linear map on the Euclidean space is symmetric.
@[deprecated Matrix.isSymmetric_toEuclideanLin_iff "use isSymmetric_toEuclideanLin_iff.symm" (since := "2026-03-30")]
theorem
Matrix.isHermitian_iff_isSymmetric
{𝕜 : Type u_1}
{n : Type u_3}
{A : Matrix n n 𝕜}
[RCLike 𝕜]
[Fintype n]
[DecidableEq n]
:
@[simp]
theorem
LinearMap.isHermitian_toMatrix_iff
{n : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[Fintype n]
[DecidableEq n]
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{f : E →ₗ[𝕜] E}
(b : OrthonormalBasis n 𝕜 E)
:
A linear map is symmetric iff the corresponding matrix with an orthonormal basis is Hermitian.