feat(topology/continuous_function/units): basic results about units in `C(α, β)` (#12687)
feat(topology/continuous_function/units): basic results about units in `C(α, β)` (#12687)

This establishes a few facts about units in `C(α, β)` including the equivalence `C(α, βˣ) ≃ C(α, β)ˣ`. Moreover, when `β` is a complete normed field, we show that the spectrum of `f : C(α, β)` is precisely `set.range f`.






leanprover-community/mathlib,leanprover-community/mathlib