mathlib3

e618cfe3 - feat(topology/continuous_function/bounded): register instances of `star` structures (#10570)

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.