OAI/Combinatorics/Progressions/Estimates/FiniteProductImageDecay.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteProductCharacter line 16
  2. def OAI.Erdos3.finiteProductCharacterCoordinate line 25
  3. theorem OAI.Erdos3.finiteProductCharacter_single line 31
  4. theorem OAI.Erdos3.finiteProductCharacter_injective line 40
  5. theorem OAI.Erdos3.finiteProductCharacter_decomposition line 49
  6. theorem OAI.Erdos3.finiteProductCharacter_order line 60
  7. theorem OAI.Erdos3.finiteImageCharacteristic_product line 71
  8. theorem OAI.Erdos3.finiteImageCharacteristic_product_decay line 80
  9. theorem OAI.Erdos3.finiteProductCharacterCoordinate_order_dvd line 98
  10. theorem OAI.Erdos3.finiteProductCharacterCoordinate_coprime line 109
  11. theorem OAI.Erdos3.finiteImageCharacteristic_crt_decay line 121