Commit 2025-11-19 17:42 3f3cd98c
View on Github →feat(Dynamics/Ergodic): add ergodic_of_ergodic_semiconj (#31793)
Adds the theorem MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconj, showing that the ergodicity property can be pushed along a semiconjugacy.