OAI/NumberTheory/PowerFree/IntegerPatches.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.totalDegree_int_map line 16
  2. theorem OAI.QuarticPowerFree.eval_int_map line 22
  3. theorem OAI.QuarticPowerFree.integer_patch_step line 27
  4. def OAI.QuarticPowerFree.EquationLock line 63
  5. theorem OAI.QuarticPowerFree.PointOn.mono line 68
  6. theorem OAI.QuarticPowerFree.equationLock_of_determined line 72
  7. theorem OAI.QuarticPowerFree.EquationLock.of_filter line 84
  8. def OAI.QuarticPowerFree.patchNextDegree line 96
  9. def OAI.QuarticPowerFree.patchDegreeBudget line 98
  10. def OAI.QuarticPowerFree.patchCountBudget line 102
  11. theorem OAI.QuarticPowerFree.le_patchDegreeBudget line 106
  12. theorem OAI.QuarticPowerFree.one_le_patchCountBudget line 111
  13. def OAI.QuarticPowerFree.GoodPatchPiece line 114
  14. def OAI.QuarticPowerFree.PatchPieceCovers line 120
  15. theorem OAI.QuarticPowerFree.zeroDim_patch_cover line 124
  16. theorem OAI.QuarticPowerFree.list_flatMap_length_le line 145
  17. theorem OAI.QuarticPowerFree.bounded_integer_patch_cover line 155
  18. def OAI.QuarticPowerFree.evaluationSpace line 261
  19. def OAI.QuarticPowerFree.evaluationCell line 268
  20. theorem OAI.QuarticPowerFree.evaluationSpace_antitone line 273
  21. theorem OAI.QuarticPowerFree.evaluationCell_antitone line 278
  22. theorem OAI.QuarticPowerFree.evaluationCell_eq_of_congruent line 286
  23. theorem OAI.QuarticPowerFree.proper_cut_patch_cover line 305