Commit 2024-07-08 17:08 2d5abb42

feat(ContinuousFunctionalCalculus): When cfc is applied to a function that maps zero to zero, it is equal to cfcₙ (#14432) This PR shows that cfcₙ f a = cfc f a whenever f maps zero to zero (and the usual continuity conditions apply). This required refactoring the proof that a unital CFC implies a non-unital one, since we need reuse the objects that were defined locally inside the proof.