mathlib

47ad6800 - feat(measure_theory/interval_integral): integration by substitution / change of variables (#7273)

feat(measure_theory/interval_integral): integration by substitution / change of variables (#7273) Given that `f` has a derivative at `f'` everywhere on `interval a b`, `∫ x in a..b, (g ∘ f) x * f' x = ∫ x in f a..f b, g x`. Co-authored by @ADedecker