Theorem MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconj

Modification history

2025-11-19 17:42
Mathlib/Dynamics/Ergodic/Ergodic.lean
feat(Dynamics/Ergodic): add `ergodic_of_ergodic_semiconj` (#31793) …
Added MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconjView on Github →