Commit 2025-08-27 07:58 f790fa27

View on Github →

chore: rename MeasureTheory.measure_zero_iff_ae_notMem (#29003)

Estimated changes

Modified Mathlib/Dynamics/Ergodic/Conservative.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

Modified Mathlib/MeasureTheory/OuterMeasure/AE.lean

added theorem MeasureTheory.measure_eq_zero_iff_ae_notMem

deleted theorem MeasureTheory.measure_zero_iff_ae_notMem

Modified Mathlib/Probability/Distributions/Uniform.lean

Modified Mathlib/Probability/Kernel/Basic.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean