mathlib

95413e23 - feat(measure_theory/group/*): various lemmas about invariant measures (#13539)

feat(measure_theory/group/*): various lemmas about invariant measures (#13539) * Make the `measurable_equiv` argument to `measure_preserving.symm` explicit. This argument is cannot always be deduced from the other explicit arguments (which can be seen form the changes in `src/measure_theory/constructions/pi.lean`). * From the sphere eversion project * Required for convolutions