OAI/Combinatorics/Progressions/Geometry/FiniteSumCoordinate.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coordinateAdditionInputs line 11
  2. theorem OAI.Erdos3.coordinateAdditionInputs_sum line 15
  3. theorem OAI.Erdos3.coordinateAdditionInputs_left line 19
  4. theorem OAI.Erdos3.coordinateAdditionInputs_right line 22
  5. def OAI.Erdos3.coordinateAdditionProduct line 25
  6. def OAI.Erdos3.coordinateConstantInput line 40
  7. def OAI.Erdos3.coordinatePairInput line 43
  8. theorem OAI.Erdos3.coordinatePairInput_sum line 47
  9. theorem OAI.Erdos3.coordinatePairInput_left line 52
  10. theorem OAI.Erdos3.coordinatePairInput_right line 55
  11. def OAI.Erdos3.finiteSumCoordinateInput line 71
  12. def OAI.Erdos3.finiteTermCoordinateInput line 74
  13. def OAI.Erdos3.finiteSumCoordinateHom line 77
  14. def OAI.Erdos3.finiteTermCoordinateHom line 85
  15. theorem OAI.Erdos3.finiteSumCoordinateInput_one line 92