Commit 2025-03-20 06:35 e4cf8333

View on Github →

chore: review of erw in MeasureTheory/ (#23127)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Decomposition/Jordan.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Group/Prod.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

Modified Mathlib/MeasureTheory/Measure/GiryMonad.lean

Modified Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean