mathlib

a4831583 - feat(topology/algebra/group): continuity of action of a group on its own coset space (#11772)

feat(topology/algebra/group): continuity of action of a group on its own coset space (#11772) Given a subgroup `Γ` of a topological group `G`, there is an induced scalar action of `G` on the coset space `G ⧸ Γ`, and there is also an induced topology on `G ⧸ Γ`. We prove that this action is continuous in each variable, and, if the group `G` is locally compact, also jointly continuous. Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>