Theorem MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_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.preErgodic_of_preErgodic_semiconjView on Github →