Commit 2024-05-29 20:55 36a9da67

View on Github →

feat: restriction of the non-unital continuous functional calculus to a scalar subring (#13327) Co-authored by: @ADedecker

depends on: #13323

Estimated changes

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

added theorem QuasispectrumRestricts.cfcₙHom_eq_restrict

added theorem QuasispectrumRestricts.cfcₙ_eq_restrict

added theorem QuasispectrumRestricts.closedEmbedding_nonUnitalStarAlgHom

added def QuasispectrumRestricts.homeomorph

added def QuasispectrumRestricts.nonUnitalStarAlgHom

added theorem QuasispectrumRestricts.nonUnitalStarAlgHom_id