Commit 2025-10-07 15:26 1dcc3037

View on Github →

feat: define curveIntegral (#24754) Define the integral of a 1-form along a (piecewise smooth) path in a normed space. This is a step towards a formalization of the Poincaré lemma for 1-forms.

Estimated changes

added theorem CurveIntegrable.neg
added theorem CurveIntegrable.refl
added theorem CurveIntegrable.smul
added theorem CurveIntegrable.zero
added def CurveIntegrable
added theorem curveIntegrable_symm
added theorem curveIntegralFun_add
added theorem curveIntegralFun_cast
added theorem curveIntegralFun_def
added theorem curveIntegralFun_neg
added theorem curveIntegralFun_refl
added theorem curveIntegralFun_smul
added theorem curveIntegralFun_sub
added theorem curveIntegralFun_symm
added theorem curveIntegralFun_zero
added theorem curveIntegral_add
added theorem curveIntegral_cast
added theorem curveIntegral_def
added theorem curveIntegral_fun_add
added theorem curveIntegral_fun_neg
added theorem curveIntegral_fun_smul
added theorem curveIntegral_fun_sub
added theorem curveIntegral_fun_zero
added theorem curveIntegral_neg
added theorem curveIntegral_refl
added theorem curveIntegral_segment
added theorem curveIntegral_smul
added theorem curveIntegral_sub
added theorem curveIntegral_symm
added theorem curveIntegral_trans
added theorem curveIntegral_zero
deleted theorem IntervalIntegrable.congr