Theorem cfcₙHom_eq_cfcₙHom_of_cfcHom

Modification history

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_cfcHom View on Github →