# Commit 2021-02-13 19:32 ac19b4a9

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