Theorem TopologicalGroup.isOpenMap_iff_nhds_one

Modification history

2025-09-16 23:57
Mathlib/Topology/Algebra/Group/Basic.lean
chore: `TopologicalGroup.isOpenMap_iff_nhds_one` -> `IsTopologicalGroup.isOpenMap_iff_nhds_one` (#29721)
Deleted TopologicalGroup.isOpenMap_iff_nhds_oneView on Github →
2025-02-11 07:39
Mathlib/Topology/Algebra/Group/Basic.lean
feat(Topology/Algebra): monoids with open units (#21298)
Added TopologicalGroup.isOpenMap_iff_nhds_oneView on Github →