Theorem MonoidHom.preErgodic_of_dense_iUnion_preimage_one

Modification history

2024-09-15 19:00
Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
feat(Dynamics/Ergodic): ergodicity of `(a * ·)` (#16577)
Added MonoidHom.preErgodic_of_dense_iUnion_preimage_oneView on Github →