Theorem intervalIntegral.integral_deriv_comp_smul_deriv'

Modification history

2026-03-23 08:24

Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean

feat: more versions of the change of variables formula for monotone functions (#36855) …

Deleted intervalIntegral.integral_deriv_comp_smul_deriv'View on Github →

2025-03-10 16:50

Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

refactor(MeasureTheory/Integral): split FundThmCalculus and fix late import (#22788) …

Modified intervalIntegral.integral_deriv_comp_smul_deriv'View on Github →

2023-06-07 18:05

Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

feat: port MeasureTheory.Integral.FundThmCalculus (#4773)

Added intervalIntegral.integral_deriv_comp_smul_deriv'View on Github →