Closed subgroup theorem

Stream: Is there code for X?

[Paradoxy]

ClosedSubgroup is defined in Mathlib.Topology.Algebra.Group.ClosedSubgroup but I am unable to find Closed subgroup theorem, is it proven somewhere? If not, is there any on-going work on it?

[Michael Rothgang]

We certainly don't have embedded (smooth/topological/...) submanifolds yet, so at the moment you cannot state that theorem in mathlib yet. I'm actively working on that, though: what would help me is getting my PRs reviewed. There's a thread in PR reviews about this ("smooth embeddings")