Commit 2025-05-06 14:42 f7834315

View on Github →

chore(DivergenceTheorem): fix names (#24624) The statements are about fderiv, not fderivWithin.

Estimated changes

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean

Modified Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

added theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable

deleted theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable

added theorem MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable'

added theorem MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable

added theorem MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv

deleted theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable'

deleted theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable

deleted theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁

deleted theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂

deleted theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_of_equiv

added theorem MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le

deleted theorem MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le

added theorem MeasureTheory.integral_eq_of_hasDerivAt_off_countable

added theorem MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_le

deleted theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable

deleted theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable_of_le