Theorem QuasispectrumRestricts.cfcₙHom_eq_restrict

Modification history

2026-02-23 18:16
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …
Modified QuasispectrumRestricts.cfcₙHom_eq_restrictView on Github →
2024-10-03 20:47
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
chore: Rename `UniformEmbedding` to `IsUniformEmbedding` (#17295) …
Modified QuasispectrumRestricts.cfcₙHom_eq_restrictView on Github →
2024-05-29 20:55
Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean
feat: restriction of the non-unital continuous functional calculus to a scalar subring (#13327) …
Added QuasispectrumRestricts.cfcₙHom_eq_restrictView on Github →