mathlib

f9dc84ed - 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`.