feat: port Dynamics.Circle.RotationNumber.TranslationNumber (#3433)

leanprover-community · Apr 17, 2023 · b000aad · b000aad
1 parent 0ec9f46
commit b000aad
Show file tree

Hide file tree

Showing 2 changed files with 1,036 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1124,6 +1124,7 @@ import Mathlib.Deprecated.Subfield
 import Mathlib.Deprecated.Subgroup
 import Mathlib.Deprecated.Submonoid
 import Mathlib.Deprecated.Subring
+import Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
 import Mathlib.Dynamics.FixedPoints.Basic
 import Mathlib.Dynamics.FixedPoints.Topology
 import Mathlib.Dynamics.Flow