OAI/Combinatorics/Progressions/Geometry/SquarefreeSupportPermutation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.squarefreeSupportModule line 11
2. theorem OAI.Erdos3.mem_squarefreeSupportModule line 24
3. theorem OAI.Erdos3.squarefreeSupportModule_mono line 28
4. theorem OAI.Erdos3.squarefreeSupportModule_eq_top line 34
5. theorem OAI.Erdos3.squarefreeSupportModule_eq_bot line 40
6. theorem OAI.Erdos3.squarefreeMonomial_mem_support line 49
7. theorem OAI.Erdos3.squarefreePermute_mem_support_iff line 66
8. theorem OAI.Erdos3.SquarefreeIndex.permutedBound_le_iff line 84