mathlib3

7be21e09 - feat(topology/algebra/group): quotient by a closed subgroup is regular (#13278)