Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes