mathlib3

da76d218 - feat(measure_theory/measure/haar_quotient): Pushforward of Haar measure is Haar (#11593)

feat(measure_theory/measure/haar_quotient): Pushforward of Haar measure is Haar (#11593) For `G` a topological group with discrete subgroup `Γ`, the pushforward to the coset space `G ⧸ Γ` of the restriction of a both left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure on `G ⧸ Γ`. When `Γ` is normal (and under other certain suitable conditions), we show that this measure is the Haar measure on the quotient group `G ⧸ Γ`. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Eric <ericrboidi@gmail.com>