Commit 2021-06-14 21:50 615af755
View on Github →feat(measure_theory/interval_integral): integral_deriv_comp_mul_deriv (#7141)
∫ x in a..b, (g ∘ f) x * f' x, where f' is derivative of f and g is the derivative of some function (the latter qualification allowing us to compute the integral directly by FTC-2)