OAI/Combinatorics/Progressions/Geometry/CyclicProgressionCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.minParam line 15
2. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.unitParam line 17
3. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.predParam line 21
4. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.minParam_apply line 30
5. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.unitParam_apply_self line 33
6. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.unitParam_apply_ne line 38
7. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.predParam_apply_self line 43
8. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.predParam_apply_ne line 48
9. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.eval_eq_eval_minParam_add_sum line 54
10. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.eval_unitParam line 67
11. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.eval_predParam_add_eval_unitParam line 83
12. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.sum_predParam_add_one line 124