Commit 2024-03-07 21:32 861e4fd3

feat: define ContinuousMapZero (#11220) This defines the type of continuous maps C(X, R)₀ (notation is scoped) that map zero to zero. This type is used to define the continuous functional calculus for non-unital algebras. While it is possible to use a term, namely an ideal of C(X, R) given by the kernel of the evaluation (at zero) map, this caused problems with type class inference.