Skip to content

Commit fe7e9d0

Browse files
committed
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`.
1 parent cd9849d commit fe7e9d0

File tree

4 files changed

+531
-493
lines changed

4 files changed

+531
-493
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2470,6 +2470,7 @@ import Mathlib.MeasureTheory.Decomposition.Jordan
24702470
import Mathlib.MeasureTheory.Decomposition.Lebesgue
24712471
import Mathlib.MeasureTheory.Decomposition.RadonNikodym
24722472
import Mathlib.MeasureTheory.Decomposition.SignedHahn
2473+
import Mathlib.MeasureTheory.Decomposition.SignedLebesgue
24732474
import Mathlib.MeasureTheory.Decomposition.UnsignedHahn
24742475
import Mathlib.MeasureTheory.Function.AEEqFun
24752476
import Mathlib.MeasureTheory.Function.AEEqFun.DomAct

0 commit comments

Comments
 (0)