Commit 2024-09-09 09:33 2eb00cae

View on Github →

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

Estimated changes

Modified Mathlib/Dynamics/Ergodic/Action/Basic.lean

Modified Mathlib/Dynamics/Ergodic/AddCircle.lean

Modified Mathlib/Dynamics/Ergodic/Ergodic.lean

modified structure Ergodic

added theorem PreErgodic.ae_empty_or_univ

modified structure PreErgodic

deleted theorem QuasiErgodic.ae_empty_or_univ'

added theorem QuasiErgodic.aeconst_set₀

modified structure QuasiErgodic