Skip to content

Commit b000aad

Browse files
urkudurkud
committed
feat: port Dynamics.Circle.RotationNumber.TranslationNumber (#3433)
1 parent 0ec9f46 commit b000aad

2 files changed

Lines changed: 1036 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1124,6 +1124,7 @@ import Mathlib.Deprecated.Subfield
11241124
import Mathlib.Deprecated.Subgroup
11251125
import Mathlib.Deprecated.Submonoid
11261126
import Mathlib.Deprecated.Subring
1127+
import Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
11271128
import Mathlib.Dynamics.FixedPoints.Basic
11281129
import Mathlib.Dynamics.FixedPoints.Topology
11291130
import Mathlib.Dynamics.Flow

0 commit comments

Comments
 (0)