Commit 2024-05-04 18:40 15c55c21
View on Github →refactor: new definition of eigenvectorUnitary (#11363)
This file contains the spectral theorem for Hermitian matrices and nearby relevant theorems. We rewrote the file, recasting the natural eigenvector basis matrix as a unitary called eigenvectorUnitary, and removed a lot of defeq abuse that the original file contained, considerably simplifying things.