Theorem Ergodic.symm

Modification history

2026-09-18 11:47
Mathlib/Dynamics/Ergodic/Ergodic.lean
feat(Dynamics/Ergodic): stronger PreErgodic definition (#43484) …
Modified Ergodic.symmView on Github →
2025-04-02 13:27
Mathlib/Dynamics/Ergodic/Ergodic.lean
feat(Ergodic): add `Ergodic.symm` (#23566)
Added Ergodic.symmView on Github →