Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 17:02 7679be23

View on Github →

feat(dynamics/ergodic/add_circle): ergodicity of zsmul on the additive circle (#17544)

Estimated changes

Modified src/algebra/hom/iterate.lean

added theorem pow_iterate

added theorem zpow_iterate

Modified src/data/real/ennreal.lean

added theorem ennreal.div_eq_one_iff

Created src/data/set/pointwise/iterate.lean

added theorem smul_eq_self_of_preimage_zpow_eq_self

Created src/dynamics/ergodic/add_circle.lean

added theorem add_circle.ae_empty_or_univ_of_forall_vadd_eq_self

added theorem add_circle.ergodic_nsmul

added theorem add_circle.ergodic_zsmul

Modified src/measure_theory/constructions/prod.lean

Modified src/topology/algebra/monoid.lean

added theorem filter.tendsto_nhds_within_Iio.const_mul

added theorem filter.tendsto_nhds_within_Iio.mul_const

added theorem filter.tendsto_nhds_within_Ioi.const_mul

added theorem filter.tendsto_nhds_within_Ioi.mul_const

Modified src/topology/separation.lean

modified theorem tendsto_const_nhds_iff