Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-09 09:32 df85590c

View on Github →

feat(dynamics/ergodic/add_circle): ergodicity of y ↦ n • y + x on the additive circle (#17580)

Estimated changes

Modified src/dynamics/ergodic/add_circle.lean

added theorem add_circle.ergodic_nsmul_add

added theorem add_circle.ergodic_zsmul_add

Modified src/dynamics/ergodic/ergodic.lean

added theorem measure_theory.measure_preserving.ergodic_conjugate_iff

added theorem measure_theory.measure_preserving.pre_ergodic_conjugate_iff

added theorem measure_theory.measure_preserving.pre_ergodic_of_pre_ergodic_conjugate

Modified src/dynamics/ergodic/measure_preserving.lean

deleted theorem measure_theory.measure_preserving.comp