English
A Hermitian matrix has Hermitian inverse iff the matrix is Hermitian.
Русский
Гермитова матрица имеет Hermitian обратную, если и только если сама матрица Hermitian.
LaTeX
$$$(A^{-1})^{\\mathrm{H}} = A^{-1} \\iff A^{\\mathrm{H}} = A$$$
Lean4
/-- A matrix is Hermitian iff the corresponding linear map is self adjoint. -/
theorem isHermitian_iff_isSymmetric [Fintype n] [DecidableEq n] {A : Matrix n n α} :
IsHermitian A ↔ A.toEuclideanLin.IsSymmetric :=
by
rw [LinearMap.IsSymmetric, (WithLp.toLp_surjective _).forall₂]
simp only [toEuclideanLin_toLp, Matrix.toLin'_apply, EuclideanSpace.inner_eq_star_dotProduct, WithLp.ofLp_toLp,
star_mulVec]
constructor
· rintro (h : Aᴴ = A) x y
rw [dotProduct_comm, ← dotProduct_mulVec, h, dotProduct_comm]
· intro h
ext i j
simpa [(Pi.single_star i 1).symm] using h (Pi.single i 1) (Pi.single j 1)
