no goals
α : Type u_2
β : Type ?u.4512
m : Type u_3
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
e : m ≃ n
h : IsHermitian (submatrix A ↑e ↑e)
⊢ IsHermitian A
simpa using h.submatrix e.symm