Theorem cfcₙHom_isClosedEmbedding

Modification history

2026-02-23 18:16

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

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

Modified cfcₙHom_isClosedEmbedding View on Github →

2024-10-20 13:29

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

chore: Rename `ClosedEmbedding` to `IsClosedEmbedding` (#17937) …

Added cfcₙHom_isClosedEmbedding View on Github →