Theorem: Matrix.IsHermitian.eigenvectorMatrix_inv_mul (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : LinearOrder n
inst✝² : LocallyFiniteOrderBot n
𝕜 : Type u_2
inst✝¹ : DecidableEq 𝕜
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.eigenvectorMatrixInv * hA.eigenvectorMatrix = 1
Tactic:
apply Basis.toMatrix_mul_toMatrix_flip
State after:
no goals