Theorem SeparationQuotient.nhds_mk

Modification history

2025-10-31 08:47
Mathlib/Topology/Inseparable.lean
chore: remove declarations deprecated before 2025-04-21 (#30759) …
Deleted SeparationQuotient.nhds_mkView on Github →
2025-03-23 02:21
Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean
feat(SeparationQuotient): add `IsTopologicalGroup` instance (#23225) …
Modified SeparationQuotient.nhds_mkView on Github →
2025-02-05 23:29
Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean
feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk` (#18178) …
Added SeparationQuotient.nhds_mkView on Github →