OAI/GroupTheory/PeriodicGroups/Rules/GeometricRelations.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.FiniteTable.Cell.shape_core_iff line 13
  2. lemma OAI.SourceBurnside.FiniteTable.Cell.shape_stop_iff line 17
  3. lemma OAI.SourceBurnside.FiniteTable.startsCore_shape line 20
  4. lemma OAI.SourceBurnside.FiniteTable.endsStop_shape line 28
  5. theorem OAI.SourceBurnside.FiniteTable.Survives.complete_normalize line 35
  6. lemma OAI.SourceBurnside.FiniteTable.Cell.cut_leftExternal line 47
  7. lemma OAI.SourceBurnside.FiniteTable.pair_before_core_zero line 54
  8. lemma OAI.SourceBurnside.FiniteTable.Survives.syntax_of_exterior line 68
  9. lemma OAI.SourceBurnside.FiniteTable.Survives.before_cut_end line 89
  10. theorem OAI.SourceBurnside.FiniteTable.Survives.cut_interval_normalize line 102
  11. def OAI.SourceBurnside.FiniteTable.GeomRel line 116
  12. instance OAI.SourceBurnside.FiniteTable.(instance at line 119) line 119
  13. lemma OAI.SourceBurnside.FiniteTable.Survives.geom_rel line 130
  14. def OAI.SourceBurnside.FiniteTable.beginnings line 143
  15. def OAI.SourceBurnside.FiniteTable.firstCoreCount line 145
  16. lemma OAI.SourceBurnside.FiniteTable.Survives.beginning_ranks line 147
  17. lemma OAI.SourceBurnside.FiniteTable.rank_list_bound line 162
  18. lemma OAI.SourceBurnside.FiniteTable.Survives.beginning_count_bound line 183
  19. lemma OAI.SourceBurnside.FiniteTable.firstCoreCount_eq line 202
  20. lemma OAI.SourceBurnside.FiniteTable.firstCoreCount_shape line 206
  21. lemma OAI.SourceBurnside.FiniteTable.firstCoreCount_reach line 213
  22. lemma OAI.SourceBurnside.FiniteTable.firstCoreCount_append line 217
  23. lemma OAI.SourceBurnside.FiniteTable.firstCoreCount_block line 221
  24. lemma OAI.SourceBurnside.FiniteTable.firstCoreCount_encode line 228
  25. theorem OAI.SourceBurnside.FiniteTable.Survives.token_normalization line 239
  26. def OAI.SourceBurnside.FiniteTable.Rigid.width line 261
  27. lemma OAI.SourceBurnside.FiniteTable.Rigid.width_pos line 263
  28. def OAI.SourceBurnside.FiniteTable.Rigid.position line 265
  29. def OAI.SourceBurnside.FiniteTable.Rigid.shape line 269
  30. def OAI.SourceBurnside.FiniteTable.Rigid.coord line 272
  31. def OAI.SourceBurnside.FiniteTable.Rigid.block line 274
  32. def OAI.SourceBurnside.FiniteTable.Rigid.cell line 276
  33. def OAI.SourceBurnside.FiniteTable.Rigid.core line 281
  34. lemma OAI.SourceBurnside.FiniteTable.Rigid.coord_cell line 285
  35. lemma OAI.SourceBurnside.FiniteTable.Rigid.block_cell line 289
  36. lemma OAI.SourceBurnside.FiniteTable.Rigid.cell_block_coord line 295
  37. lemma OAI.SourceBurnside.FiniteTable.Rigid.position_core_iff line 300
  38. lemma OAI.SourceBurnside.FiniteTable.Rigid.position_stop_iff line 310
  39. lemma OAI.SourceBurnside.FiniteTable.Rigid.shape_core_iff line 316
  40. lemma OAI.SourceBurnside.FiniteTable.Rigid.shape_stop_iff line 321
  41. lemma OAI.SourceBurnside.FiniteTable.Rigid.canonicalBlock_get line 325
  42. lemma OAI.SourceBurnside.FiniteTable.Rigid.canonicalBlock_ofFn line 338
  43. def OAI.SourceBurnside.FiniteTable.Rigid.encoded line 346
  44. lemma OAI.SourceBurnside.FiniteTable.Rigid.encoded_cell line 349
  45. lemma OAI.SourceBurnside.FiniteTable.Rigid.encoded_ofFn line 353
  46. def OAI.SourceBurnside.FiniteTable.Rigid.Layout line 366
  47. lemma OAI.SourceBurnside.FiniteTable.Rigid.layout_encoded line 368
  48. def OAI.SourceBurnside.FiniteTable.Rigid.decoded line 374
  49. lemma OAI.SourceBurnside.FiniteTable.Rigid.decoded_eq line 378
  50. lemma OAI.SourceBurnside.FiniteTable.Rigid.decoded_encoded line 383
  51. lemma OAI.SourceBurnside.FiniteTable.Rigid.layout_core line 394
  52. lemma OAI.SourceBurnside.FiniteTable.Rigid.layout_core_iff line 400
  53. lemma OAI.SourceBurnside.FiniteTable.Rigid.layout_stop_iff line 406
  54. lemma OAI.SourceBurnside.FiniteTable.Rigid.layout_reach line 411
  55. lemma OAI.SourceBurnside.FiniteTable.Rigid.block_mono line 420
  56. lemma OAI.SourceBurnside.FiniteTable.Rigid.block_next line 423
  57. lemma OAI.SourceBurnside.FiniteTable.Rigid.first_le_iff line 443
  58. lemma OAI.SourceBurnside.FiniteTable.Rigid.le_last_iff line 455
  59. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_left_mod line 473
  60. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_right_mod line 479
  61. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_left_cell line 483
  62. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_right_cell line 488
  63. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_block_counter line 496
  64. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_last_block line 531
  65. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_interval line 545
  66. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_size line 556
  67. def OAI.SourceBurnside.FiniteTable.Rigid.regionBlock line 568
  68. lemma OAI.SourceBurnside.FiniteTable.Rigid.regionCore_owned line 575
  69. lemma OAI.SourceBurnside.FiniteTable.Rigid.region_cell line 582
  70. lemma OAI.SourceBurnside.FiniteTable.Rigid.split_ofFn line 606
  71. lemma OAI.SourceBurnside.FiniteTable.Rigid.context_of_interval line 617
  72. theorem OAI.SourceBurnside.FiniteTable.Rigid.pivot_context line 643