Commit 2024-09-15 19:00 93d2fbb9

View on Github →

feat(Dynamics/Ergodic): ergodicity of (a * ·) (#16577)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean

added theorem DenseRange.zpow_of_ergodic_mul_left

added theorem ErgodicSMul.trans_isMinimal

added theorem MonoidHom.ergodic_of_dense_iUnion_preimage_one

added theorem MonoidHom.preErgodic_of_dense_iUnion_preimage_one

added theorem aeconst_of_dense_aestabilizer_smul

added theorem aeconst_of_dense_setOf_preimage_smul_ae

added theorem aeconst_of_dense_setOf_preimage_smul_eq

added theorem ergodic_mul_left_iff_denseRange_zpow

added theorem ergodic_mul_left_of_denseRange_pow

added theorem ergodic_mul_left_of_denseRange_zpow

added theorem ergodic_smul_of_denseRange_pow

added theorem ergodic_smul_of_denseRange_zpow