add_circle): generalise `add_circle.ae_empty_or_univ_of_forall_vadd_eq_self` slightly (#17907)

Commit

3 years ago

feat(dynamics/ergodic/add_circle): generalise `add_circle.ae_empty_or_univ_of_forall_vadd_eq_self` slightly (#17907) I need this generalised version for an application.

Author

ocfnash

Parents

1897d7de

mathlib3 ae3588fa - feat(dynamics/ergodic/add_circle): generalise `add_circle.ae_empty_or_univ_of_forall_vadd_eq_self` slightly (#17907)

mathlib3
ae3588fa - feat(dynamics/ergodic/add_circle): generalise `add_circle.ae_empty_or_univ_of_forall_vadd_eq_self` slightly (#17907)