OAI/Combinatorics/Progressions/Estimates/NativeDetectorContradiction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_selected_product_factorization line 13
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_anchored_option_product_factorization line 135
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_anchored_option_mode_factorization line 273
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_anchored_option_factors line 410
5. theorem OAI.Erdos3.PositiveShiftBasis.exists_common_product_factors line 547
6. theorem OAI.Erdos3.PositiveShiftBasis.exists_prescribed_common_factorization line 680
7. theorem OAI.Erdos3.PositiveShiftBasis.exists_native_partner_contradiction line 779
8. theorem OAI.Erdos3.PositiveShiftBasis.exists_native_partner_pair_contradiction line 854
9. theorem OAI.Erdos3.PositiveShiftBasis.exists_two_site_model_contradiction line 930
10. theorem OAI.Erdos3.PositiveShiftBasis.exists_native_detector_contradiction line 998