Zulip Chat Archive
Stream: mathlib4
Topic: Ergodic and EventuallyConst
Yury G. Kudryashov (Jul 20 2024 at 01:18):
I suggest that we redefine docs#PreErgodic etc in terms of docs#Filter.EventuallyConst. Are there any objections? @Oliver Nash @Sébastien Gouëzel
Oliver Nash (Jul 27 2024 at 11:00):
No objections!
Last updated: May 02 2025 at 03:31 UTC