α : Type u_2
β : Type ?u.47971
m : Type u_1
n : Type ?u.47977
A✝ : Matrix n n α
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : IsHermitian A⁻¹
⊢ IsHermitian A⁻¹⁻¹
α : Type u_2
β : Type ?u.47971
m : Type u_1
n : Type ?u.47977
A✝ : Matrix n n α
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : IsHermitian A⁻¹
⊢ IsHermitian A
rw [← inv_inv_of_invertible A]
no goals
α : Type u_2
β : Type ?u.47971
m : Type u_1
n : Type ?u.47977
A✝ : Matrix n n α
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : IsHermitian A⁻¹
⊢ IsHermitian A⁻¹⁻¹
exact IsHermitian.inv h