OAI/GroupTheory/PeriodicGroups/Rules/WordComponents.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SourceBurnside.FiniteTable.Shape line 12
  2. def OAI.SourceBurnside.FiniteTable.Cell.shape line 16
  3. lemma OAI.SourceBurnside.FiniteTable.Unary.shape line 19
  4. lemma OAI.SourceBurnside.FiniteTable.Binary.shape line 23
  5. lemma OAI.SourceBurnside.FiniteTable.replacement_shape line 35
  6. lemma OAI.SourceBurnside.FiniteTable.step_shape line 45
  7. lemma OAI.SourceBurnside.FiniteTable.reach_shape line 50
  8. def OAI.SourceBurnside.FiniteTable.Exterior line 56
  9. lemma OAI.SourceBurnside.FiniteTable.exterior_of_syntax line 60
  10. lemma OAI.SourceBurnside.FiniteTable.Coherent.owner_right line 81
  11. lemma OAI.SourceBurnside.FiniteTable.Coherent.owner_left line 107
  12. theorem OAI.SourceBurnside.FiniteTable.Coherent.owner line 137
  13. def OAI.SourceBurnside.FiniteTable.Component.members line 148
  14. lemma OAI.SourceBurnside.FiniteTable.Component.mem_iff line 150
  15. lemma OAI.SourceBurnside.FiniteTable.Component.nonempty line 152
  16. def OAI.SourceBurnside.FiniteTable.Component.left line 153
  17. def OAI.SourceBurnside.FiniteTable.Component.right line 154
  18. lemma OAI.SourceBurnside.FiniteTable.Component.connected_left line 156
  19. lemma OAI.SourceBurnside.FiniteTable.Component.connected_right line 159
  20. lemma OAI.SourceBurnside.FiniteTable.Component.left_le line 162
  21. lemma OAI.SourceBurnside.FiniteTable.Component.le_right line 165
  22. lemma OAI.SourceBurnside.FiniteTable.Component.left_le_self line 168
  23. lemma OAI.SourceBurnside.FiniteTable.Component.self_le_right line 170
  24. lemma OAI.SourceBurnside.FiniteTable.Component.left_le_right line 172
  25. lemma OAI.SourceBurnside.FiniteTable.Component.interval line 174
  26. lemma OAI.SourceBurnside.FiniteTable.Component.exterior_left line 184
  27. lemma OAI.SourceBurnside.FiniteTable.Component.exterior_right line 200
  28. lemma OAI.SourceBurnside.FiniteTable.Component.first line 212
  29. lemma OAI.SourceBurnside.FiniteTable.Component.last line 221
  30. def OAI.SourceBurnside.FiniteTable.Component.size line 234
  31. lemma OAI.SourceBurnside.FiniteTable.Component.size_pos line 236
  32. def OAI.SourceBurnside.FiniteTable.Component.offset line 240
  33. lemma OAI.SourceBurnside.FiniteTable.Component.connected_offset line 248
  34. lemma OAI.SourceBurnside.FiniteTable.Component.offset_adjacent line 257
  35. lemma OAI.SourceBurnside.FiniteTable.Component.offset_internal line 260
  36. lemma OAI.SourceBurnside.FiniteTable.Component.offset_first_iff line 268
  37. lemma OAI.SourceBurnside.FiniteTable.Component.offset_last_iff line 282
  38. def OAI.SourceBurnside.FiniteTable.Component.region line 298
  39. lemma OAI.SourceBurnside.FiniteTable.Component.offset_injective line 315
  40. lemma OAI.SourceBurnside.FiniteTable.Component.offset_surjective line 322
  41. lemma OAI.SourceBurnside.FiniteTable.Component.sum_offset line 330
  42. lemma OAI.SourceBurnside.FiniteTable.Component.total_region line 343
  43. lemma OAI.SourceBurnside.FiniteTable.Component.region_holds line 354
  44. def OAI.SourceBurnside.FiniteTable.Cell.positionRank line 367
  45. def OAI.SourceBurnside.FiniteTable.Cell.progress line 370
  46. lemma OAI.SourceBurnside.FiniteTable.Cell.rank_lt line 373
  47. lemma OAI.SourceBurnside.FiniteTable.Cell.progress_mod line 380
  48. lemma OAI.SourceBurnside.FiniteTable.Cell.progress_div line 384
  49. lemma OAI.SourceBurnside.FiniteTable.Cell.progress_step line 388
  50. lemma OAI.SourceBurnside.FiniteTable.Region.progress_step line 406
  51. lemma OAI.SourceBurnside.FiniteTable.Region.progress_mono line 412
  52. lemma OAI.SourceBurnside.FiniteTable.Region.first_progress line 427
  53. lemma OAI.SourceBurnside.FiniteTable.Region.last_progress line 432
  54. lemma OAI.SourceBurnside.FiniteTable.Region.progress_surjective line 438
  55. lemma OAI.SourceBurnside.FiniteTable.Region.core_unique line 461
  56. lemma OAI.SourceBurnside.FiniteTable.Region.core_rank_le line 486
  57. def OAI.SourceBurnside.FiniteTable.Region.locate line 494
  58. lemma OAI.SourceBurnside.FiniteTable.Region.locate_progress line 496
  59. lemma OAI.SourceBurnside.FiniteTable.Region.locate_rank line 499
  60. lemma OAI.SourceBurnside.FiniteTable.Region.locate_pos line 503
  61. lemma OAI.SourceBurnside.FiniteTable.Region.locate_block line 512
  62. lemma OAI.SourceBurnside.FiniteTable.Region.locate_unique line 520
  63. def OAI.SourceBurnside.FiniteTable.Region.slot line 526
  64. def OAI.SourceBurnside.FiniteTable.Region.certificate line 528
  65. def OAI.SourceBurnside.FiniteTable.Region.read line 529
  66. lemma OAI.SourceBurnside.FiniteTable.Region.block_lt line 534
  67. lemma OAI.SourceBurnside.FiniteTable.Region.sum_read line 541
  68. lemma OAI.SourceBurnside.FiniteTable.Region.addressed_total line 583
  69. lemma OAI.SourceBurnside.FiniteTable.Region.holds_iff line 588