Theorem CurveIntegrable.fun_zero

Modification history

2025-12-22 21:59
Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
refactor: use "@[to_fun]" to generate some lemmas (#32830)
Deleted CurveIntegrable.fun_zeroView on Github →
2025-10-07 15:26
Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
feat: define `curveIntegral` (#24754) …
Added CurveIntegrable.fun_zeroView on Github →