Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.closure_eq_of_is_closed

Modification history

2023-03-02 00:11
src/topology/algebra/ring/basic.lean
chore(topology/algebra/ring): split into 2 files (#18532)
Modified ideal.closure_eq_of_is_closedView on Github →
2022-10-24 18:38
src/topology/algebra/ring.lean
feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons (#16719) …
Added ideal.closure_eq_of_is_closedView on Github →