Commit 2022-02-11 18:25 da76d218

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 ⧸ Γ.