Theorem cfcₙHom_eq_cfcₙHom_of_cfcHom

Modification history

2026-02-23 18:16
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …
Modified cfcₙHom_eq_cfcₙHom_of_cfcHomView on Github →
2025-01-17 03:48
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643) …
Modified cfcₙHom_eq_cfcₙHom_of_cfcHomView 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ₙHom_eq_cfcₙHom_of_cfcHomView on Github →