Theorems · Theorem · dynamical systems
CircleDeg1Lift.translationNumber_translate
∀ (x : ℝ), (↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x))).translationNumber = x
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Equivstatement · cited by 8,337
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- MonoidHomstatement · cited by 3,629
- Unitsstatement · cited by 2,804
- add_zeroproof · cited by 2,707
- Filter.atTopproof · cited by 2,405
- Units.valstatement and proof · cited by 1,966
- Multiplicativestatement · cited by 875
- Multiplicative.ofAddstatement and proof · cited by 237
Cited by2
Results whose statement or proof uses this declaration.
- CircleDeg1Lift.translationNumber_le_of_le_addproof · cited by 1
- CircleDeg1Lift.le_translationNumber_of_add_leproof · cited by 1