OAI/GroupTheory/PeriodicGroups/Algebra/PacketIntervals.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.PacketIntervals.total line 11
  2. lemma OAI.SourceBurnside.PacketIntervals.total_nil line 13
  3. lemma OAI.SourceBurnside.PacketIntervals.total_cons line 14
  4. lemma OAI.SourceBurnside.PacketIntervals.total_append line 16
  5. lemma OAI.SourceBurnside.PacketIntervals.total_perm line 19
  6. def OAI.SourceBurnside.PacketIntervals.floorSplit line 22
  7. def OAI.SourceBurnside.PacketIntervals.ceilSplit line 29
  8. lemma OAI.SourceBurnside.PacketIntervals.floorSplit_join line 35
  9. lemma OAI.SourceBurnside.PacketIntervals.ceilSplit_join line 45
  10. lemma OAI.SourceBurnside.PacketIntervals.floorSplit_bound line 57
  11. lemma OAI.SourceBurnside.PacketIntervals.floorSplit_next line 69
  12. lemma OAI.SourceBurnside.PacketIntervals.floorSplit_prefix line 84
  13. lemma OAI.SourceBurnside.PacketIntervals.ceilSplit_zero line 104
  14. lemma OAI.SourceBurnside.PacketIntervals.ceilSplit_reaches line 107
  15. lemma OAI.SourceBurnside.PacketIntervals.ceilSplit_before line 121
  16. lemma OAI.SourceBurnside.PacketIntervals.ceilSplit_prefix line 141
  17. lemma OAI.SourceBurnside.PacketIntervals.ceilSplit_empty_or_before line 169
  18. lemma OAI.SourceBurnside.PacketIntervals.ceilSplit_overshoot line 183
  19. lemma OAI.SourceBurnside.PacketIntervals.floorSplit_defect line 200
  20. structure OAI.SourceBurnside.PacketIntervals.Selection line 215
  21. def OAI.SourceBurnside.PacketIntervals.Selection.join line 221
  22. def OAI.SourceBurnside.PacketIntervals.select line 223
  23. lemma OAI.SourceBurnside.PacketIntervals.select_join line 228
  24. lemma OAI.SourceBurnside.PacketIntervals.select_total line 232
  25. lemma OAI.SourceBurnside.PacketIntervals.select_before_bound line 237
  26. lemma OAI.SourceBurnside.PacketIntervals.select_inside_bound line 242
  27. lemma OAI.SourceBurnside.PacketIntervals.select_permute line 262
  28. lemma OAI.SourceBurnside.PacketIntervals.total_le_length_mul line 280
  29. theorem OAI.SourceBurnside.PacketIntervals.select_long line 290
  30. def OAI.SourceBurnside.DirectCancellation.spell line 318
  31. lemma OAI.SourceBurnside.DirectCancellation.spell_append line 320
  32. lemma OAI.SourceBurnside.DirectCancellation.length_spell line 323
  33. lemma OAI.SourceBurnside.DirectCancellation.spell_perm line 329
  34. lemma OAI.SourceBurnside.DirectCancellation.nodup_of_spell_nodup line 332
  35. lemma OAI.SourceBurnside.DirectCancellation.interval_sublist line 340
  36. lemma OAI.SourceBurnside.DirectCancellation.select_spelling_sublist line 352
  37. lemma OAI.SourceBurnside.DirectCancellation.erased_eq_of_perm_uniform line 378
  38. def OAI.SourceBurnside.DirectCancellation.eval line 390
  39. lemma OAI.SourceBurnside.DirectCancellation.eval_append line 392
  40. lemma OAI.SourceBurnside.DirectCancellation.eval_perm_uniform line 395
  41. def OAI.SourceBurnside.DirectCancellation.pickPacket line 412
  42. lemma OAI.SourceBurnside.DirectCancellation.pickPacket_join line 419
  43. lemma OAI.SourceBurnside.DirectCancellation.reordered_perm line 423
  44. lemma OAI.SourceBurnside.DirectCancellation.pickPacket_stable line 430
  45. lemma OAI.SourceBurnside.DirectCancellation.pickPacket_same_value line 463
  46. def OAI.SourceBurnside.DirectCancellation.candidates line 489
  47. lemma OAI.SourceBurnside.DirectCancellation.mem_candidates line 492
  48. def OAI.SourceBurnside.DirectCancellation.chunkSum line 501
  49. theorem OAI.SourceBurnside.DirectCancellation.chunkSum_eq_zero_of_ranges line 506