mathlib

1a862493 - feat(measure_theory/function/l1_space): add `integrable_smul_measure` (#13922)

feat(measure_theory/function/l1_space): add `integrable_smul_measure` (#13922) * add `integrable_smul_measure`, an `iff` version of `integrable.smul_measure`; * add `integrable_average`, an `iff` version of `integrable.to_average`.