OAI/Combinatorics/Progressions/Lattices/NativeRetainedIntegerMultilinearQuadruples.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.cyclicBranchOffset line 11
  2. theorem OAI.Erdos3.cyclicTranslationOffset_eq_branch line 14
  3. theorem OAI.Erdos3.exists_two_shift_integer_interval line 18
  4. theorem OAI.Erdos3.exists_fourPoint_integer_interval line 88
  5. def OAI.Erdos3.NativeCrossWitnesses.integerLower line 153
  6. def OAI.Erdos3.NativeCrossWitnesses.integerProduct line 155
  7. theorem OAI.Erdos3.NativeCrossWitnesses.integerLower_val line 158
  8. theorem OAI.Erdos3.NativeCrossWitnesses.integerProduct_val line 160
  9. theorem OAI.Erdos3.NativeCrossWitnesses.extension_quadruple_integer line 166
  10. theorem OAI.Erdos3.NativeCrossWitnesses.exists_integer_quadruple_interval line 179
  11. theorem OAI.Erdos3.NativeCrossWitnesses.integerProduct_fourPoint_factorization line 201
  12. theorem OAI.Erdos3.NativeCrossWitnesses.exists_integer_quadruple_interval_budget line 214
  13. structure OAI.Erdos3.NativeIntegerQuadrupleWitness line 253
  14. def OAI.Erdos3.NativeCorrelationStructure.multilinearFactor line 291
  15. theorem OAI.Erdos3.exists_integer_multilinear_quadruples line 299
  16. theorem OAI.Erdos3.exists_integer_multilinear_quadruples_with_equivalence line 393