Commit 2025-09-16 23:42 540f0820
View on Github →chore(Analysis/CStarAlgebra/ContinuousFunctionalCalculus): deprecate some duplicate declarations (#29731)
At a certain point, we refactored SpectrumRestricts so that it was a synonym of QuasispectrumRestricts and these duplicate lemmas hadn't yet been removed.