OAI/Combinatorics/Progressions/Estimates/GroupReductionFactors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.compact_representatives_step line 16
2. theorem OAI.Erdos3.exists_compact_representatives_of_reductions line 30
3. theorem OAI.Erdos3.compactSpace_quotient_of_representatives line 56
4. theorem OAI.Erdos3.exists_representative_factors_of_reductions line 81