Theorem Matrix.IsHermitian.mulVec_eigenvectorBasis

Modification history

2024-05-04 18:40

Mathlib/LinearAlgebra/Matrix/Spectrum.lean

refactor: new definition of `eigenvectorUnitary` (#11363) …

Modified Matrix.IsHermitian.mulVec_eigenvectorBasis View on Github →

2023-12-18 20:33

Mathlib/LinearAlgebra/Matrix/Spectrum.lean

feat(LinearAlgebra/Matrix/PosDef): unique positive semidef square root (#8809) …

Added Matrix.IsHermitian.mulVec_eigenvectorBasis View on Github →