Commit 2025-03-23 02:21 eab25444
View on Github →feat(SeparationQuotient): add IsTopologicalGroup instance (#23225)
Also move nhds_mk and deprecate it in favor of map_mk_nhds.
feat(SeparationQuotient): add IsTopologicalGroup instance (#23225)
Also move nhds_mk and deprecate it in favor of map_mk_nhds.