mathlib
822244f7 - refactor(measure_theory/group/basic): rename and split (#11952)

Commit
3 years ago
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. ```lean 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 ```
Author
Parents
Loading