mathlib3

32735ca2 - feat(measure_theory/measure_space): add mutually singular measures (#8605)

feat(measure_theory/measure_space): add mutually singular measures (#8605) This PR defines `mutually_singular` for measures. This is useful for Jordan and Lebesgue decomposition.