mathlib

54236f5a - feat(topology/continuous_function/compact): `cstar_ring` instance on `C(α, β)` when `α` is compact (#14437)

feat(topology/continuous_function/compact): `cstar_ring` instance on `C(α, β)` when `α` is compact (#14437) We define the star operation on `C(α, β)` by applying `β`'s star operation pointwise. In the case when `α` is compact, then `C(α, β)` has a norm, and we show that it is a `cstar_ring`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>