mathlib

432da5f8 - feat(measure_theory/integration): add lintegral_with_density_eq_lintegral_mul (#4350)

feat(measure_theory/integration): add lintegral_with_density_eq_lintegral_mul (#4350) This is Exercise 1.2.1 from Terence Tao's "An Epsilon of Room" Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>