Def SpectrumRestricts.homeomorph

Modification history

2024-05-24 22:26

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean

feat: golf SpectrumRestricts.closedEmbedding_starAlgHom using uniform trickery (#13014)

Added SpectrumRestricts.homeomorph View on Github →