Commit 2024-05-24 22:26 c9ee63a2

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

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

modified theorem SpectrumRestricts.cfcHom_eq_restrict

modified theorem SpectrumRestricts.cfc_eq_restrict

added def SpectrumRestricts.homeomorph