feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons

[j-loreaux]

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

---

[alreadydone]

Just a heads up that #16860 is introducing a maximal_spectrum definition.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16709~~
• ~~leanprover-community/mathlib#16713~~
• ~~leanprover-community/mathlib#16714~~
• ~~leanprover-community/mathlib#16677~~
• ~~leanprover-community/mathlib#16663~~
• ~~leanprover-community/mathlib#16721~~
• ~~leanprover-community/mathlib#16722~~
• ~~leanprover-community/mathlib#16801~~ By Dependent Issues (🤖). Happy coding!

[ocfnash]

Thanks!

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests