Commit 2022-04-08 02:06 5e98dc1c

feat(topology/continuous_function/zero_at_infty): add more instances for zero_at_infty_continuous_map and establish C₀ functorial properties (#13196) This adds more instances for the type C₀(α, β) of continuous functions vanishing at infinity. Notably, these new instances include its non-unital ring, normed space and star structures, culminating with cstar_ring when β is a cstar_ring which is also a topological_ring. In addition, this establishes functorial properties of C₀(-, β) for various choices of algebraic categories involving β. The domain of these (contravariant) functors is the category of topological spaces with cocompact continuous maps, and the functor applied to a cocompact map is given by pre-composition.