Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-07 10:37 44400c99

View on Github →

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.

Estimated changes