mathlib

a9db7ced - chore(measure_theory/{bochner_integration, simple_func_dense}): Move construction of embedding of L1 simple funcs (#8185)

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.