Theorem IsTopologicalGroup.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)
Added IsTopologicalGroup.isOpenMap_iff_nhds_oneView on Github →