Commit 2025-09-26 13:55 06c7bee2
View on Github →chore(Analysis/Normed/Algebra/Spectrum): split file and reduce imports (#29978) This file is currently a very heavy import as it relies on Liouville's theorem to prove that the spectrum is nonempty, as well as the Cauchy integral formula to prove Gelfand's formula. We split out these results into a separate file to significantly reduce the import burden.