Theorem LinearMap.IsSymmetric.card_filter_eigenvalues_eq

Modification history

2026-03-10 21:47
Mathlib/Analysis/InnerProductSpace/Spectrum.lean
chore(Analysis/InnerProductSpace): remove a hypothesis from LinearMap.IsSymmetric.card_filter_eigenvalues_eq (#36106) …
Modified LinearMap.IsSymmetric.card_filter_eigenvalues_eqView on Github →
2026-02-10 19:29
Mathlib/Analysis/InnerProductSpace/Spectrum.lean
feat(Analysis/InnerProductSpace): multiplicity of LinearMap.IsSymmetric.eigenvalues (#34660) …
Added LinearMap.IsSymmetric.card_filter_eigenvalues_eqView on Github →