Commit 2021-12-09 19:38 e618cfe3

feat(topology/continuous_function/bounded): register instances of star structures (#10570) Prove that the bounded continuous functions which take values in a normed C⋆-ring themselves form a C⋆-ring. Moreover, if the codomain is a normed algebra and a star module over a normed ⋆-ring, then so are the bounded continuous functions. Thus the bounded continuous functions form a C⋆-algebra when the codomain is a C⋆-algebra.