mathlib3

592f769e - feat(dynamics/circle): define translation number of a lift of a circle homeo (#2974)

feat(dynamics/circle): define translation number of a lift of a circle homeo (#2974) Define a structure `circle_deg1_lift`, a function `translation_number : circle_deg1_lift → ℝ`, and prove some basic properties