Commit 2026-03-10 21:47 31e19511
View on Github →chore(Analysis/InnerProductSpace): remove a hypothesis from LinearMap.IsSymmetric.card_filter_eigenvalues_eq (#36106)
Use proof by cases to remove an unnecessary hypothesis from LinearMap.IsSymmetric.card_filter_eigenvalues_eq and the related private LinearMap.IsSymmetric.card_filter_unsortedEigenvalues_eq. This required proving a statement similar to LinearMap.IsSymmetric.hasEigenvalue_eigenvalues but for unsortedEigenvalues.