Theorem Ergodic.of_preimage_eq

Modification history

2026-09-18 11:47
Mathlib/Dynamics/Ergodic/Ergodic.lean
feat(Dynamics/Ergodic): stronger PreErgodic definition (#43484) …
Added Ergodic.of_preimage_eqView on Github →