Commit 2022-02-12 08:07 822244f7

refactor(measure_theory/group/basic): rename and split (#11952)

• Rename measure_theory/group/basic -> measure_theory/group/measure. It was not the bottom file in this folder in the import hierarchy (arithmetic is below it).
• Split off some results to measure_theory/group/integration. This reduces imports in some files, and makes the organization more clear. Furthermore, I will add some integrability results and more integrals in a follow-up PR.
• Prove a general instance pi.is_mul_left_invariant
• Remove lemmas specifically about volume on real in favor on the general lemmas.

real.map_volume_add_left -> map_add_left_eq_self
real.map_volume_pi_add_left -> map_add_left_eq_self
real.volume_preimage_add_left -> measure_preimage_add
real.volume_pi_preimage_add_left -> measure_preimage_add
real.map_volume_add_right -> map_add_right_eq_self 
real.volume_preimage_add_right -> measure_preimage_add_right