Theorem Matrix.IsHermitian.star_mul_self_mul_eq_diagonal

Modification history

2025-11-11 22:41
Mathlib/Analysis/Matrix/Spectrum.lean
chore(Analysis/Matrix/Spectrum): change `spectral_theorem` to use `conjStarAlgAut` map (#31322)
Deleted Matrix.IsHermitian.star_mul_self_mul_eq_diagonalView on Github →
2024-05-04 18:40
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
refactor: new definition of `eigenvectorUnitary` (#11363) …
Added Matrix.IsHermitian.star_mul_self_mul_eq_diagonalView on Github →