# Commit 2023-05-18 23:40 fd5edc43

View on Github →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`

.