OAI/NumberTheory/PowerFree/RegularBlocks.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.independent_many_regular line 14
  2. lemma OAI.QuarticPowerFree.adaptiveStates_precomp line 50
  3. def OAI.QuarticPowerFree.selectedBlocks line 60
  4. lemma OAI.QuarticPowerFree.selectedBlocks_update line 64
  5. theorem OAI.QuarticPowerFree.regular_adaptive_blocks line 73
  6. def OAI.QuarticPowerFree.cumulativeBlockPrimes line 160
  7. theorem OAI.QuarticPowerFree.cumulativeBlockPrimes_mono line 163
  8. def OAI.QuarticPowerFree.pathDegreeBudget line 171
  9. def OAI.QuarticPowerFree.physicalKernel line 175
  10. def OAI.QuarticPowerFree.physicalNext line 180
  11. def OAI.QuarticPowerFree.PhysicalState line 187
  12. theorem OAI.QuarticPowerFree.physicalKernel_mono line 191
  13. theorem OAI.QuarticPowerFree.physical_step line 198
  14. theorem OAI.QuarticPowerFree.physical_path_good line 225
  15. theorem OAI.QuarticPowerFree.physical_rank_mono_stable line 247
  16. theorem OAI.QuarticPowerFree.physical_uniform_minor_height line 263
  17. theorem OAI.QuarticPowerFree.physical_regular_blocks line 280