Structure Ergodic

Modification history

2024-09-09 09:33

Mathlib/Dynamics/Ergodic/Ergodic.lean

refactor(Ergodic): redefine using `EventuallyConst` (#16281)

Modified Ergodic View on Github →

2023-05-10 07:35

Mathlib/Dynamics/Ergodic/Ergodic.lean

feat: port Dynamics.Ergodic.Ergodic (#3879)

Added Ergodic View on Github →