Theorem TopologicalGroup.isOpenMap_iff_nhds_one

Modification history

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 →