Commit 2022-05-06 09:15 95413e23

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