Commit 2024-10-30 20:23 c6c4ad2c

View on Github →

feat(Topology/Group): Open normal subgroup in clopen nhds of one (#18377) Proving that there is always an open normal subgroup in a clopen nhd of compact topological group

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/ClopenNhdofOne.lean

added theorem TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

added structure TopologicalAddGroup.addNegClosureNhd

added theorem TopologicalGroup.exist_mul_closure_nhd

added theorem TopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one

added theorem TopologicalGroup.exists_mulInvClosureNhd

added structure TopologicalGroup.mulInvClosureNhd