Commit 2021-11-02 14:14 796a051a

feat(measure_theory/decomposition/lebesgue): more on Radon-Nikodym derivatives (#10070) We show that the density in the Lebesgue decomposition theorem (aka the Radon-Nikodym derivative) is unique. Previously, uniqueness of the absolutely continuous part was known, but not of its density. We also show that the Radon-Nikodym derivative is almost everywhere finite. Plus some cleanup of the whole file.