mathlib

55b81f8b - feat(measure_theory): measure preserving maps and integrals (#10326)

feat(measure_theory): measure preserving maps and integrals (#10326) If `f` is a measure preserving map, then `∫ y, g y ∂ν = ∫ x, g (f x) ∂μ`. It was two rewrites with the old API (`hf.map_eq`, then a lemma about integral over map measure); it's one `rw` now. Also add versions for special cases when `f` is a measurable embedding (in this case we don't need to assume measurability of `g`).