Commit 2025-04-14 13:54 d85717c5

View on Github →

chore(DivergenceTheorem): drop some CompleteSpace assumptions (#24021)

Estimated changes

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean

Modified Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

modified theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable

modified theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable_of_le