mathlib

fd5edc43 - chore(measure_theory/{constructions/prod,measure/lebesgue}): split (#19039)

chore(measure_theory/{constructions/prod,measure/lebesgue}): split (#19039) Reorganize some files in measure theory, with the goal of removing the dependence of Lebesgue measure on the Bochner integral. `measure_theory/constructions/prod` is split into `prod/basic` and `prod/integral`; the former imports the Lebesgue integral but not the Bochner integral. `measure_theory/measure/haar` is renamed `measure_theory/measure/haar/basic`. `measure_theory/measure/haar_of_inner` is renamed `measure_theory/measure/haar/inner_product_space`. `measure_theory/measure/haar_of_basis` is renamed `measure_theory/measure/haar/of_basis`. `measure_theory/measure/lebesgue` is split into `measure_theory/measure/lebesgue/basic` and `measure_theory/measure/lebesgue/integral`, with the former not importing the Bochner integral. `measure_theory/measure/complex_lebesgue` is renamed `measure_theory/measure/lebesgue/complex`. `measure_theory/measure/haar_lebesgue` is split into `measure_theory/measure/lebesgue/eq_haar` and `measure_theory/measure/haar/normed_space`, with the former not importing the Bochner integral. A few lemmas about Haar measure in normed spaces or fields are also moved from `measure_theory/group/measure` to the newly-created `measure_theory/measure/haar/normed_space`, since the former no longer imports `normed_space`.