mathlib3

dbb2b558 - feat(measure_theory/interval_integral): more on integral_comp (#7030)

feat(measure_theory/interval_integral): more on integral_comp (#7030) I replace `integral_comp_mul_right_of_pos`, `integral_comp_mul_right_of_neg`, and `integral_comp_mul_right` with a single lemma.