Commit 2025-10-18 14:55 e568f0d0

feat: a topological group acts on itself properly (#30387) Both on the left and right, and the same is true (essentially by inferInstance) for actions by closed subgroups. As a consequence we get that the quotient by a closed subgroup is Hausdorff (note that QuotientGroup.instT3Space requires the subgroup to be normal !).