Theorem DiscreteTopology.of_finite_of_isClosed_singleton

Modification history

2024-11-25 16:30
Mathlib/Topology/Order.lean
feat: ring with discrete PrimeSpectrum (#18891) …
Added DiscreteTopology.of_finite_of_isClosed_singletonView on Github →