Theorem intervalIntegral.integral_unitInterval_deriv_eq_sub

Modification history

2026-10-31 22:39
Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean
chore: remove straightforward redundant theorem hypotheses (#45526) …
Modified intervalIntegral.integral_unitInterval_deriv_eq_subView on Github →
2024-03-28 10:26
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
chore: Rename `IsROrC` to `RCLike` (#10819) …
Modified intervalIntegral.integral_unitInterval_deriv_eq_subView on Github →
2023-12-07 20:36
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
feat: add a version of FTC-2 with an integral over the unit interval (#8615) …
Added intervalIntegral.integral_unitInterval_deriv_eq_subView on Github →