Commit 2025-11-11 18:33 4d8e83ea
View on Github →chore(LinearAlgebra/Matrix): import less analysis (#31480)
Move the definition of eigenvalues of hermitian matrices to Analysis.Matrix, and the corresponding lemmas about positive (semi)definite matrices too. Some lemmas could be generalised instead of moved, and I have done so.
Ultimately, it would be great for LinearAlgebra.Matrix to import no analysis at all. But this is a longer term goal.