Commit 2026-09-22 17:00 f9c849af
View on Github →chore(Analysis/Spectrum/Real): deprecate a duplicate lemma (#44081) The hypotheses of this lemma are overly strong, and we already have this theorem elsewhere. Moreover, this lemma is unused.
chore(Analysis/Spectrum/Real): deprecate a duplicate lemma (#44081) The hypotheses of this lemma are overly strong, and we already have this theorem elsewhere. Moreover, this lemma is unused.