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_of_cfcHom_map_quasispectrum