Commit 2025-11-11 22:41 b4288117

View on Github →

chore(Analysis/Matrix/Spectrum): change spectral_theorem to use conjStarAlgAut map (#31322)

Estimated changes

Modified Mathlib/Algebra/Star/Unitary.lean

added theorem Unitary.isUnit_coe

Modified Mathlib/Algebra/Star/UnitaryStarAlgAut.lean

added theorem Unitary.conjStarAlgAut_mul_apply

added theorem Unitary.conjStarAlgAut_star_apply

Modified Mathlib/Analysis/Matrix/PosDef.lean

modified theorem Matrix.IsHermitian.posDef_iff_eigenvalues_pos

modified theorem Matrix.PosSemidef.trace_eq_zero_iff

Modified Mathlib/Analysis/Matrix/Spectrum.lean

added theorem Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary

modified theorem Matrix.IsHermitian.rank_eq_rank_diagonal

deleted theorem Matrix.IsHermitian.star_mul_self_mul_eq_diagonal

Modified Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean