Theorem MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugate

Modification history

2025-11-19 17:42
Mathlib/Dynamics/Ergodic/Ergodic.lean
feat(Dynamics/Ergodic): add `ergodic_of_ergodic_semiconj` (#31793) …
Deleted MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugateView on Github →
2023-05-10 07:35
Mathlib/Dynamics/Ergodic/Ergodic.lean
feat: port Dynamics.Ergodic.Ergodic (#3879)
Added MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugateView on Github →