Commit 2021-07-04 09:30 a9db7ced

chore(measure_theory/{bochner_integration, simple_func_dense}): Move construction of embedding of L1 simple funcs (#8185) At the moment, there is a low-level construction in measure_theory/simple_func_dense for the approximation of an element of L1 by simple functions, and this is generalized to a more abstract version (with a normed space L1.simple_func and a dense linear embedding of this into L1) in measure_theory/bochner_integration. #8114 generalized the low-level construction, and I am thinking of rewriting the more abstract version to apply to Lp, too. But since this will all be more generally useful than in the construction of the Bochner integral, and since the Bochner integral file is very long, I propose moving all this material into measure_theory/simple_func_dense. This PR shows what it would look like. There are no mathematical changes.