mathlib3

c9f6b6f0 - feat(analysis/calculus/monotone): a monotone function is differentiable almost everywhere (#16549)

feat(analysis/calculus/monotone): a monotone function is differentiable almost everywhere (#16549) The proof is an almost direct consequence of results on differentiation of measures that are already in mathlib.