Theorem isometry_cfcHom

Modification history

2026-02-23 18:16

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean

refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …

Modified isometry_cfcHom View on Github →

2024-10-27 21:51

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean

feat: isometric continuous functional calculi (#17837)

Added isometry_cfcHom View on Github →