Commit 2024-08-16 23:11 ff84cbdb

feat: better proof of spectral permanence (#15603) This uses a much cleaner argument than the previous one in order to prove the spectral permanence property of C*-algebras. The argument now goes through some generic results for Banach algebras, a corollary of which applies to selfadjoint elements. The old results which led to spectral permanence have been removed, although the spectral permanence results themselves remain unchanged (except that they have been moved into Analysis.CStarAlgebra.Spectrum from Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic, which seems a better home). Some module documentation has also been updated.