Theorem: Matrix.IsHermitian.hasEigenvector_eigenvectorBasis (CvxLean/Lib/Math/LinearAlgebra/Matrix/Spectrum.lean)

State before:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
i : n
⊢ Module.End.HasEigenvector (toLin' A) (↑(hA.eigenvalues i)) (hA.eigenvectorBasis i)
Tactic:
simp only [IsHermitian.eigenvectorBasis, OrthonormalBasis.coe_reindex]
State after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
i : n
⊢ Module.End.HasEigenvector (toLin' A) (↑(hA.eigenvalues i))
    ((⇑(⋯.eigenvectorBasis ⋯) ∘ ⇑(Fintype.equivOfCardEq ⋯).symm) i)

State before:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
i : n
⊢ Module.End.HasEigenvector (toLin' A) (↑(hA.eigenvalues i))
    ((⇑(⋯.eigenvectorBasis ⋯) ∘ ⇑(Fintype.equivOfCardEq ⋯).symm) i)
Tactic:
apply LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis
State after:
no goals