OAI/Combinatorics/Progressions/Nilpotent/CyclicNiltestDetection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.boxNiltestDetection_succ line 14
2. theorem OAI.Erdos3.exists_boxNiltestDetection line 92
3. theorem OAI.Erdos3.exists_intervalNiltestDetection line 117
4. def OAI.Erdos3.CyclicNiltestDetection line 158
5. theorem OAI.Erdos3.cyclicNiltestDetection_zero line 171
6. theorem OAI.Erdos3.exists_cyclicNiltestDetection_succ line 181
7. theorem OAI.Erdos3.exists_cyclicNiltestDetection line 234