Theorem ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable

Modification history

2025-11-24 23:37
Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean
feat(Analysis): Poincaré lemma for 1-forms (#24019)
Added ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countableView on Github →