OAI/Combinatorics/TreeEdit/CircleTree.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TreeEdit.TorusTree.point line 11
  2. lemma OAI.TreeEdit.TorusTree.point_period line 13
  3. lemma OAI.TreeEdit.TorusTree.point_mul line 18
  4. lemma OAI.TreeEdit.TorusTree.nsmul_point_eq line 25
  5. lemma OAI.TreeEdit.TorusTree.point_toAddCircle line 28
  6. lemma OAI.TreeEdit.TorusTree.circle_period_lower line 32
  7. lemma OAI.TreeEdit.TorusTree.nearby_unique line 40
  8. lemma OAI.TreeEdit.TorusTree.grid_nearby_unique line 65
  9. lemma OAI.TreeEdit.TorusTree.product_positive line 82
  10. lemma OAI.TreeEdit.TorusTree.sparse_order line 85
  11. lemma OAI.TreeEdit.TorusTree.sparse_bad_prime line 120
  12. lemma OAI.TreeEdit.TorusTree.prime_list_event line 163
  13. lemma OAI.TreeEdit.TorusTree.dense_grid_bad line 202
  14. lemma OAI.TreeEdit.TorusTree.dense_grid_eligible line 221
  15. lemma OAI.TreeEdit.TorusTree.coefficient_circle line 235
  16. def OAI.TreeEdit.TorusTree.group line 253
  17. lemma OAI.TreeEdit.TorusTree.group_card line 255
  18. def OAI.TreeEdit.TorusTree.Config line 267
  19. instance OAI.TreeEdit.TorusTree.configFintype line 271
  20. instance OAI.TreeEdit.TorusTree.configNonempty line 277
  21. def OAI.TreeEdit.TorusTree.period line 282
  22. def OAI.TreeEdit.TorusTree.coefficient line 285
  23. def OAI.TreeEdit.TorusTree.Good line 289
  24. lemma OAI.TreeEdit.TorusTree.period_pos line 296
  25. lemma OAI.TreeEdit.TorusTree.group_prime_dvd line 299
  26. lemma OAI.TreeEdit.TorusTree.cast_hom_val line 303
  27. lemma OAI.TreeEdit.TorusTree.coefficient_shift line 308
  28. lemma OAI.TreeEdit.TorusTree.fixed_residue_failure line 329
  29. lemma OAI.TreeEdit.TorusTree.conditional_good_failure line 403
  30. theorem OAI.TreeEdit.TorusTree.good_probability line 435