Commit 2024-03-12 19:14 1c3f3619

feat: uniqueness of the continuous functional calculus (#11256) This establishes uniqueness of the continuous functional calculus for unital algebras. When the scalar ring is ℝ or ℂ, this follows immediately from Stone-Weierstrass, but for ℝ≥0, we need to reuse the result for ℝ. This is tricky, as we need to upgrade an ℝ≥0-algebra homomorphism (with domain C((s : Set ℝ≥0), ℝ≥0)) to a ℝ-algebra homomorphism (with domain C(((↑) '' s : Set ℝ), ℝ)). This is the reason the UniqueContinuousFunctionalCalculus class exists in the first place, as opposed to simply appealing directly to Stone-Weierstrass to prove StarAlgHom.ext_continuousMap.