Mathlib v3 is deprecated. Go to Mathlib v4

Theorem weak_dual.character_space.continuous_map_eval_bijective

Modification history

2022-10-24 18:38
src/topology/continuous_function/ideals.lean
feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons (#16719) …
Added weak_dual.character_space.continuous_map_eval_bijectiveView on Github →