α : Type u_2
β : Type ?u.3927
m : Type ?u.3930
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian A
α : Type u_2
β : Type ?u.3927
m : Type ?u.3930
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
⊢ IsHermitian Aᵀ → IsHermitian A
intro h
α : Type u_2
β : Type ?u.3927
m : Type ?u.3930
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian Aᵀᵀ
α : Type u_2
β : Type ?u.3927
m : Type ?u.3930
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian A
rw [← transpose_transpose A]
no goals
α : Type u_2
β : Type ?u.3927
m : Type ?u.3930
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian Aᵀᵀ
exact IsHermitian.transpose h