Theorem Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary

Modification history

2025-11-11 22:41
Mathlib/Analysis/Matrix/Spectrum.lean
chore(Analysis/Matrix/Spectrum): change `spectral_theorem` to use `conjStarAlgAut` map (#31322)
Added Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitaryView on Github →