Commit 2026-09-09 21:26 aac9be8f

feat: a locally closed subgroup is closed (#42501) We show that, in a topological group, a subgroup which is locally closed at one of its points is closed. We use this to reprove the fact that a discrete subgroup of a Hausdorff group is closed, without appealing to the theory of uniform spaces. Notes about Topology/Algebra/IsUniformGroup/DiscreteSubgroup:

• it no longer requires the theory of uniform spaces, hence should be moved
• the import increase comes, I believe, from the fact that Topology/Algebra/OpenSubgroup imports the basic theory of topological rings, which should be fixed.