mathlib
b4a2991c - feat(dynamics/ergodic): define measure preserving maps (#6764)

Commit

4 years ago

feat(dynamics/ergodic): define measure preserving maps (#6764) Also prove some missing lemmas about measures.

Author

urkud

Parents