OAI/Combinatorics/Progressions/Linear/CommonRankCoefficientCorrections.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_common_rank_relation_budget line 9
2. theorem OAI.Erdos3.exists_native_common_rank_budget line 15
3. theorem OAI.Erdos3.exists_rank_common_data_budget line 38
4. theorem OAI.Erdos3.exists_common_rank_interval_data line 76
5. structure OAI.Erdos3.NativeRankRelation.CommonData line 156
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.spaces_mem_candidates line 170
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.horizontalImage_eq line 177
8. def OAI.Erdos3.NativeRankRelation.CommonData.mono line 184
9. theorem OAI.Erdos3.NativeRankRelation.CommonData.mono_quadruples line 191
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.mono_spaces line 193
11. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_common_denominator line 218
12. def OAI.Erdos3.NativeRankRelation.CommonData.horizontal line 278
13. theorem OAI.Erdos3.NativeRankRelation.CommonData.horizontal_frequency line 282
14. theorem OAI.Erdos3.NativeRankRelation.CommonData.sunflower_bracket line 302
15. theorem OAI.Erdos3.NativeRankRelation.CommonData.sunflower_representatives line 317
16. theorem OAI.Erdos3.exists_common_rank_relation line 347
17. theorem OAI.Erdos3.exists_native_common_rank_relation line 421
18. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_bounded_coefficient_corrections line 472