no goals
α : Type u_2
β : Type ?u.46849
m : Type u_1
n : Type ?u.46855
A✝ : Matrix n n α
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : IsHermitian A
⊢ IsHermitian A⁻¹
simp [IsHermitian, conjTranspose_nonsing_inv, hA.eq]