Commit 2026-02-10 19:29 17d3cb51
View on Github →feat(Analysis/InnerProductSpace): multiplicity of LinearMap.IsSymmetric.eigenvalues (#34660)
If T is a symmetric linear map and μ : 𝕜, then μ appears somewhere in the list LinearMap.IsSymmetric.eigenvalues a number of times equal to the dimension of the eigenspace of μ.
Discussion for this PR and the related PR #34362 can be found here: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/LinearMap.2EIsSymmetric.2Eeigenvalues.20has.20all.20the.20eigenvalues/with/571092190