Commit 2022-03-16 08:21 50691e59

chore(measure_theory/function): split files strongly_measurable and simple_func_dense (#12711) The files strongly_measurable and simple_func_dense contain general results, and results pertaining to the L^p space. We move the results regarding L^p to new files, to make sure that the main parts of the files can be imported earlier in the hierarchy. This is needed for a forthcoming integral refactor.