α : Type u_2
β : Type ?u.3659
m : Type ?u.3662
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian A
⊢ (Matrix.map Aᵀ star)ᵀ = Aᵀ
α : Type u_2
β : Type ?u.3659
m : Type ?u.3662
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian A
⊢ IsHermitian Aᵀ
rw [IsHermitian, conjTranspose, transpose_map]
no goals
α : Type u_2
β : Type ?u.3659
m : Type ?u.3662
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian A
⊢ (Matrix.map Aᵀ star)ᵀ = Aᵀ
exact congr_arg Matrix.transpose h