Commit 2021-02-13 19:32 ac19b4a9

refactor(measure_theory/l1_space): remove one of the two definitions of L1 space (#6058) Currently, we have two independent versions of the L^1 space in mathlib: one coming from the general family of L^p spaces, the other one is an ad hoc construction based on the integrable predicate used in the construction of the Bochner integral. We remove the second construction, and use instead the L^1 space coming from the family of L^p spaces to construct the Bochner integral. Still, we keep the integrable predicate as it is generally useful, and show that it coincides with the mem_Lp 1 predicate.