Commit 2023-05-18 23:40 fd5edc43

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.