Theorem TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one

Modification history

2025-02-16 15:19

Mathlib/Topology/Algebra/ClopenNhdofOne.lean

chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)

Deleted TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one View on Github →

2024-10-30 20:23

Mathlib/Topology/Algebra/ClopenNhdofOne.lean

feat(Topology/Group): Open normal subgroup in clopen nhds of one (#18377) …

Added TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one View on Github →