Theorem Matrix.IsHermitian.transpose_eigenvectorMatrix_apply

Modification history

2024-05-04 18:40
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
refactor: new definition of `eigenvectorUnitary` (#11363) …
Deleted Matrix.IsHermitian.transpose_eigenvectorMatrix_applyView on Github →
2023-08-08 16:37
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
feat: Positivity/Nonnegativity of Eigenvalues of PosDef/PosSemidef Matrices (#6368) …
Added Matrix.IsHermitian.transpose_eigenvectorMatrix_applyView on Github →