mathlib3

44400c99 - feat(dynamics/circle/rotation_number): translation numbers define a group action up to a semiconjugacy (#5138)

feat(dynamics/circle/rotation_number): translation numbers define a group action up to a semiconjugacy (#5138) Formalize a theorem by Étienne Ghys: given two lifts `f₁`, `f₂` of actions of a group `G` on the circle by orientation preserving homeomorphisms to the real line, assume that for each `g : G` the translation numbers of `f₁ g` and `f₂ g` are equal. Then the actions are semiconjugate by a (possibly discontinuous) circle map. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>