Theorem IntervalIntegrable.congr

Modification history

2025-10-07 15:26
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
feat: define `curveIntegral` (#24754) …
Deleted IntervalIntegrable.congrView on Github →
2025-08-13 12:33
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
refactor(Intervalintegral): generalise to enorms (#27418) …
Modified IntervalIntegrable.congrView on Github →
2024-12-01 09:59
Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
feat(NumberTheory): Abel summation (#19289) …
Added IntervalIntegrable.congrView on Github →