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