OAI/Combinatorics/Progressions/Lattices/IntervalIntegerVectorAPFree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.APFree.integer_nonnegative_pullback line 12
2. theorem OAI.Erdos3.integerBox_unit_expect line 61
3. def OAI.Erdos3.APFreeInterval.integerIndicator line 83
4. theorem OAI.Erdos3.APFreeInterval.integerIndicator_nat line 86
5. theorem OAI.Erdos3.APFreeInterval.integerIndicator_mem_Icc line 90
6. theorem OAI.Erdos3.APFreeInterval.integerIndicator_mean line 94
7. theorem OAI.Erdos3.APFreeInterval.integerIndicator_apFree line 100