OAI/Analysis/IrrationalRotation/Product/IndependentRotation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.IndependentRotation.irrational_finsupp_rat_sum line 15
2. theorem OAI.Invariant233.IndependentRotation.irrational_coordinate line 29
3. theorem OAI.Invariant233.IndependentRotation.irrational_finsupp_int_sum line 34
4. theorem OAI.Invariant233.IndependentRotation.int_mul_character_ne_integer line 49
5. theorem OAI.Invariant233.IndependentRotation.zsmul_ne_zero_of_irrational line 55
6. theorem OAI.Invariant233.IndependentRotation.product_rotation_free line 63
7. theorem OAI.Invariant233.IndependentRotation.circle_exp_ne_one_of_irrational line 75
8. theorem OAI.Invariant233.IndependentRotation.character_eigenvalue_ne_one line 84