α : Type u_2
β : Type ?u.2918
m : Type ?u.2921
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ IsHermitian A
α : Type u_2
β : Type ?u.2918
m : Type ?u.2921
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
⊢ (∀ (i j : n), star (A j i) = A i j) → IsHermitian A
intro h
case a.h
α : Type u_2
β : Type ?u.2918
m : Type ?u.2921
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j
α : Type u_2
β : Type ?u.2918
m : Type ?u.2921
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ IsHermitian A
ext (i j)
no goals
case a.h
α : Type u_2
β : Type ?u.2918
m : Type ?u.2921
n : Type u_1
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j
exact h i j