Theorem Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric

Modification history

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