Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 20:08 f9dc84ed

View on Github →

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.

Estimated changes