# Commit 2023-07-28 12:48 3b522651

View on Github →feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863)
We prove the "unfolding trick": Given a subgroup `Γ`

of a group `G`

, the integral of a function `f`

on `G`

times the lift to `G`

of a function `g`

on the coset space `G ⧸ Γ`

with respect to a right-invariant measure `μ`

on `G`

, is equal to the integral over the coset space of the automorphization of `f`

times `g`

.
We also prove the following simplified version: Given a subgroup `Γ`

of a group `G`

, the integral of a function `f`

on `G`

with respect to a right-invariant measure `μ`

is equal to the integral over the coset space `G ⧸ Γ`

of the automorphization of `f`

.
A question: is it possible to deduce `ae_strongly_measurable (quotient_group.automorphize f) μ_𝓕`

from `ae_strongly_measurable f μ`

(as opposed to assuming it as a hypothesis in the main theorem)? It seems quite plausible...