Commit 2021-06-09 10:12 47ad6800
View on Github →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