Commit 2023-05-15 16:30 24e0c854
View on Github →chore(measure_theory/{integral/set_integral,function/*}): split out inner product space material (#19019) Split out inner product space material from
measure_theory/function/lp_space
measure_theory/function/l1_space
measure_theory/integral/set_integral
into measure_theory/integral/l2_space, the only place it's used. This removes the dependence of the Bochner integral file on inner_product_space.