OAI/Combinatorics/Progressions/Lattices/PrimeStabilityTree.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.PrimeStabilityContext line 16
  2. def OAI.Erdos3.PrimeStabilityContext.moduli line 48
  3. def OAI.Erdos3.PrimeStabilityContext.workBudget line 51
  4. def OAI.Erdos3.PrimeStabilityContext.periodCap line 54
  5. def OAI.Erdos3.PrimeStabilityContext.stepCost line 57
  6. def OAI.Erdos3.PrimeStabilityContext.allowance line 60
  7. def OAI.Erdos3.PrimeStabilityContext.HasLargeSides line 63
  8. def OAI.Erdos3.PrimeStabilityContext.Good line 67
  9. structure OAI.Erdos3.PrimeStabilityContext.State line 71
  10. def OAI.Erdos3.PrimeStabilityContext.State.rank line 80
  11. theorem OAI.Erdos3.PrimeStabilityContext.moduli_pos line 84
  12. theorem OAI.Erdos3.PrimeStabilityContext.moduli_coprime line 87
  13. theorem OAI.Erdos3.PrimeStabilityContext.workBudget_nonneg line 91
  14. theorem OAI.Erdos3.PrimeStabilityContext.product_pos line 112
  15. theorem OAI.Erdos3.PrimeStabilityContext.product_le_exp_card line 115
  16. theorem OAI.Erdos3.PrimeStabilityContext.node_width line 124
  17. theorem OAI.Erdos3.PrimeStabilityContext.construction_width line 142
  18. def OAI.Erdos3.PrimeStabilityContext.State.periodBatch line 159
  19. theorem OAI.Erdos3.PrimeStabilityContext.State.periodBatch_disjoint line 162
  20. theorem OAI.Erdos3.PrimeStabilityContext.State.periodBatch_card line 167
  21. theorem OAI.Erdos3.PrimeStabilityContext.State.periods_covered line 175
  22. theorem OAI.Erdos3.PrimeStabilityContext.State.one_step_room line 182
  23. theorem OAI.Erdos3.PrimeStabilityContext.State.room_of_smaller_rank line 189
  24. theorem OAI.Erdos3.PrimeStabilityContext.State.aligned_refinement line 196
  25. theorem OAI.Erdos3.PrimeStabilityContext.State.repair_cell line 222
  26. theorem OAI.Erdos3.PrimeStabilityContext.State.local_tree line 289
  27. theorem OAI.Erdos3.PrimeStabilityContext.State.stable_tree line 355
  28. theorem OAI.Erdos3.PrimeStabilityContext.exists_stable_tree line 362
  29. theorem OAI.Erdos3.PrimeStabilityContext.exists_covering_stable_tree line 404