Theorem IsTopologicalGroup.isOpenMap_iff_nhds_one

Modification history

2026-08-24 07:44
Mathlib/Topology/Algebra/Group/Basic.lean
refactor(Topology/Algebra/Group): split long file Basic.lean (#43010) …
Modified IsTopologicalGroup.isOpenMap_iff_nhds_oneView on Github →
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 →