mathlib

1846a1f3 - feat(measure_theory/interval_integral): `abs_integral_le_integral_abs` (#7959)

feat(measure_theory/interval_integral): `abs_integral_le_integral_abs` (#7959) The absolute value of the integral of an integrable function is less than or equal to the integral of the absolute value that function.