no goals
α : Type u_2
β : Type ?u.50563
m : Type u_1
n : Type ?u.50569
A✝ : Matrix n n α
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : IsHermitian A
⊢ IsHermitian (Matrix.adjugate A)
simp [IsHermitian, adjugate_conjTranspose, hA.eq]