Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_circle.ae_empty_or_univ_of_forall_vadd_eq_self

Modification history

2022-12-14 17:11
src/dynamics/ergodic/add_circle.lean
feat(dynamics/ergodic/add_circle): generalise `add_circle.ae_empty_or_univ_of_forall_vadd_eq_self` slightly (#17907) …
Deleted add_circle.ae_empty_or_univ_of_forall_vadd_eq_selfView on Github →
2022-12-06 17:02
src/dynamics/ergodic/add_circle.lean
feat(dynamics/ergodic/add_circle): ergodicity of zsmul on the additive circle (#17544)
Added add_circle.ae_empty_or_univ_of_forall_vadd_eq_selfView on Github →