Theorem continuousFunctionalCalculus_map_id

Modification history

2026-02-23 18:16
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …
Modified continuousFunctionalCalculus_map_idView on Github →
2023-06-12 18:27
Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean
feat: port Analysis.NormedSpace.Star.ContinuousFunctionalCalculus (#4977)
Added continuousFunctionalCalculus_map_idView on Github →