English
The Coe of eigenvectorUnitary is the matrix formed by the eigenvector basis in the standard basis.
Русский
Коэффициентное представление eigenvectorUnitary совпадает с базисом собственных векторов в стандартном базисе.
LaTeX
$$$\text{eigenvectorUnitary}(h_A) = (\text{EuclideanSpace}.basisFun(n, \mathbb{K}).toBasis.toMatrix (h_A.eigenvectorBasis).toBasis)$$$
Lean4
/-- Unitary matrix whose columns are `Matrix.IsHermitian.eigenvectorBasis`. -/
noncomputable def eigenvectorUnitary {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n]
(hA : Matrix.IsHermitian A) : Matrix.unitaryGroup n 𝕜 :=
⟨(EuclideanSpace.basisFun n 𝕜).toBasis.toMatrix (hA.eigenvectorBasis).toBasis,
(EuclideanSpace.basisFun n 𝕜).toMatrix_orthonormalBasis_mem_unitary (eigenvectorBasis hA)⟩
