Commit 2023-11-08 22:44 fe7e9d03

View on Github →

chore: split MeasureTheory.Decomposition.Lebesgue (#8272) Put all results about decomposition of signed measures into a new file. This does not significantly change the imports of the original file, because signed measures are used in the proof of the Lebesgue decomposition theorem for Measure.

Estimated changes