OAI/Analysis/IrrationalRotation/Sampling/CircleCharacterDynamics.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleCharacterDynamics.representative_coe line 13
2. theorem OAI.Invariant233.CircleCharacterDynamics.coe_representative line 16
3. theorem OAI.Invariant233.CircleCharacterDynamics.representative_add_real line 19
4. theorem OAI.Invariant233.CircleCharacterDynamics.zsmul_real_phase line 25
5. theorem OAI.Invariant233.CircleCharacterDynamics.character_orbit_representative line 31
6. theorem OAI.Invariant233.CircleCharacterDynamics.zsmul_rational_eq_zero line 38
7. theorem OAI.Invariant233.CircleCharacterDynamics.character_rational_translation line 51