Commit 2026-03-23 17:30 050c3f02

feat: generalize results on the range of the continuous functional calculus to avoid closed embeddings (#36908) Due to a recent refactor, the continuous functional calculus no longer requires that the homomorphism is a closed embedding, only that it is continuous and injective. Consequently, it is possible to generalize some of the results pertaining the the range of this map. In particular, the range is always contained in (thought not necessarily equal to) the closed star subalgebra generated by the element. Along the way, we provide the lemmas cfc_mem and cfcₙ_mem, which are intended to be quite useful. In particular, these show that cfcₙ f a ∈ s where s is any closed star subalgebra containing a. Moreover, they are intended to work even in the case that f : ℝ → ℝ (so we are working with the real continuous functional calculus) and s is a ℂ-subalgebra (unital or non-unital).