mathlib

63ff4532 - feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons (#16719)

feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons (#16719) This establishes the correspondence between maximal ideals of `C(X, 𝕜)` (where `X` is compact Hausdorff and `is_R_or_C 𝕜`) and the complements of singletons in `X`. This allows for the proof that the natural map from `X` to `character_space 𝕜 C(X, 𝕜)` is a homeomorphism. - [x] depends on: #16709 - [x] depends on: #16713 - [x] depends on: #16714 - [x] depends on: #16677 - [x] depends on: #16663 - [x] depends on: #16721 - [x] depends on: #16722 - [x] depends on: #16801