Commit 2022-10-24 18:38 63ff4532

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.

• depends on: #16709
• depends on: #16713
• depends on: #16714
• depends on: #16677
• depends on: #16663
• depends on: #16721
• depends on: #16722
• depends on: #16801