measure_preserving): add `measure_preserving.symm` (#9940)

Commit

4 years ago

feat(dynamics/ergodic/measure_preserving): add `measure_preserving.symm` (#9940) Also make the proof of `measure_preserving.skew_product` a bit more readable.

Author

urkud

Parents

4ea8de91

mathlib3 c20f08ed - feat(dynamics/ergodic/measure_preserving): add `measure_preserving.symm` (#9940)

mathlib3
c20f08ed - feat(dynamics/ergodic/measure_preserving): add `measure_preserving.symm` (#9940)