no goals
α : Type u_3
β : Type ?u.28730
m : Type u_1
n : Type u_2
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype m
A : Matrix m n α
⊢ IsHermitian (Aᴴ ⬝ A)
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]