mathlib

ec0b1144 - feat(measure_theory/group/prod.lean): use measure_preserving predicate (#16668)

feat(measure_theory/group/prod.lean): use measure_preserving predicate (#16668) * Also use `quasi_measure_preserving` more in various files. In particular, `ae_[strongly_]measurable.comp_measurable'` is now `.comp_quasi_measure_preserving`. * Remove lemmas that are direct consequences of `[quasi_]measure_preserving` properties. * This simplifies various proofs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>