Commit 2025-09-18 15:32 aad26963

refactor: switch to using Fact (0 ∈ s) for ContinuousMapZero.id (#29563) ContinuousMapZero is used exclusively for the non-unital continuous functional calculus. Within this scope we have an instance Zero s for s : Set R under the assumption Fact (0 ∈ s). This is somewhat reasonable because, in the most common scenario, s := quasispectrum R a, for which we can always provide this Fact instance. However, several declarations were put in place prior to this Zero instance, and they made use of a different paradigm where we take Zero s as an argument and then have another argument of the form h0 : ↑(0 : s) = (0 : R). This PR shifts that paradigm into the new regime, and I think this change is beneficial.