Theorem cfcₙ_eq_cfc

Modification history

2026-02-23 18:16
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …
Modified cfcₙ_eq_cfcView on Github →
2025-01-17 03:48
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643) …
Modified cfcₙ_eq_cfcView on Github →
2024-07-08 17:08
Mathlib/Topology/ContinuousFunction/NonUnitalFunctionalCalculus.lean
feat(ContinuousFunctionalCalculus): When `cfc` is applied to a function that maps zero to zero, it is equal to `cfcₙ` (#14432) …
Added cfcₙ_eq_cfcView on Github →