OAI/GroupTheory/UniversalGroup/UniversalPresentation.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.UniversalGroup.PresentationCode line 11
  2. abbrev OAI.UniversalFInfinity.UniversalGroup.Presented line 12
  3. abbrev OAI.UniversalFInfinity.UniversalGroup.CountableUniversal line 13
  4. instance OAI.UniversalFInfinity.UniversalGroup.(instance at line 15) line 15
  5. instance OAI.UniversalFInfinity.UniversalGroup.(instance at line 16) line 16
  6. instance OAI.UniversalFInfinity.UniversalGroup.(instance at line 20) line 20
  7. theorem OAI.UniversalFInfinity.UniversalGroup.countable_universal line 23
  8. def OAI.UniversalFInfinity.FreeConjugates.shift line 38
  9. lemma OAI.UniversalFInfinity.FreeConjugates.shift_of line 41
  10. def OAI.UniversalFInfinity.FreeConjugates.shifts line 43
  11. abbrev OAI.UniversalFInfinity.FreeConjugates.ShiftGroup line 54
  12. abbrev OAI.UniversalFInfinity.FreeConjugates.Two line 55
  13. def OAI.UniversalFInfinity.FreeConjugates.a line 56
  14. def OAI.UniversalFInfinity.FreeConjugates.p line 57
  15. def OAI.UniversalFInfinity.FreeConjugates.word line 58
  16. def OAI.UniversalFInfinity.FreeConjugates.test line 60
  17. lemma OAI.UniversalFInfinity.FreeConjugates.test_a line 64
  18. lemma OAI.UniversalFInfinity.FreeConjugates.test_p line 66
  19. lemma OAI.UniversalFInfinity.FreeConjugates.test_word line 69
  20. def OAI.UniversalFInfinity.FreeConjugates.inclusion line 77
  21. lemma OAI.UniversalFInfinity.FreeConjugates.test_comp line 79
  22. lemma OAI.UniversalFInfinity.FreeConjugates.inclusion_injective line 87
  23. abbrev OAI.UniversalFInfinity.CountableOvergroup.Base line 98
  24. def OAI.UniversalFInfinity.CountableOvergroup.left line 100
  25. def OAI.UniversalFInfinity.CountableOvergroup.right line 103
  26. lemma OAI.UniversalFInfinity.CountableOvergroup.left_of line 106
  27. lemma OAI.UniversalFInfinity.CountableOvergroup.right_of line 110
  28. def OAI.UniversalFInfinity.CountableOvergroup.projection line 114
  29. lemma OAI.UniversalFInfinity.CountableOvergroup.left_injective line 117
  30. lemma OAI.UniversalFInfinity.CountableOvergroup.projection_right line 120
  31. lemma OAI.UniversalFInfinity.CountableOvergroup.right_injective line 125
  32. def OAI.UniversalFInfinity.CountableOvergroup.associated line 130
  33. abbrev OAI.UniversalFInfinity.CountableOvergroup.Overgroup line 134
  34. def OAI.UniversalFInfinity.CountableOvergroup.embed line 137
  35. lemma OAI.UniversalFInfinity.CountableOvergroup.embed_injective line 139
  36. def OAI.UniversalFInfinity.CountableOvergroup.a line 142
  37. def OAI.UniversalFInfinity.CountableOvergroup.p line 143
  38. def OAI.UniversalFInfinity.CountableOvergroup.t line 144
  39. lemma OAI.UniversalFInfinity.CountableOvergroup.associated_left line 146
  40. lemma OAI.UniversalFInfinity.CountableOvergroup.generator_formula line 154
  41. lemma OAI.UniversalFInfinity.CountableOvergroup.closure_three_of_generates line 170
  42. lemma OAI.UniversalFInfinity.CountableOvergroup.closure_three line 207
  43. lemma OAI.UniversalFInfinity.CountableOvergroup.finitely_generated line 211
  44. theorem OAI.UniversalFInfinity.CountableOvergroup.countable_embeds_three_generated line 214
  45. abbrev OAI.UniversalFInfinity.ThreePresentation.Alphabet line 225
  46. abbrev OAI.UniversalFInfinity.ThreePresentation.Words line 226
  47. def OAI.UniversalFInfinity.ThreePresentation.A line 228
  48. def OAI.UniversalFInfinity.ThreePresentation.P line 229
  49. def OAI.UniversalFInfinity.ThreePresentation.T line 230
  50. def OAI.UniversalFInfinity.ThreePresentation.conjugate line 231
  51. def OAI.UniversalFInfinity.ThreePresentation.substitute line 232
  52. abbrev OAI.UniversalFInfinity.ThreePresentation.C line 236
  53. abbrev OAI.UniversalFInfinity.ThreePresentation.V line 237
  54. abbrev OAI.UniversalFInfinity.ThreePresentation.Q line 238
  55. def OAI.UniversalFInfinity.ThreePresentation.generator line 240
  56. lemma OAI.UniversalFInfinity.ThreePresentation.lift_substitute line 245
  57. lemma OAI.UniversalFInfinity.ThreePresentation.substituted_relation line 254
  58. def OAI.UniversalFInfinity.ThreePresentation.toV line 260
  59. def OAI.UniversalFInfinity.ThreePresentation.fromC line 263
  60. lemma OAI.UniversalFInfinity.ThreePresentation.fromC_of line 266
  61. lemma OAI.UniversalFInfinity.ThreePresentation.toV_comp_fromC line 272
  62. theorem OAI.UniversalFInfinity.ThreePresentation.fromC_injective line 282
  63. abbrev OAI.UniversalFInfinity.RecursiveUniversal.Word line 291
  64. abbrev OAI.UniversalFInfinity.RecursiveUniversal.Code line 292
  65. def OAI.UniversalFInfinity.RecursiveUniversal.relations line 294
  66. def OAI.UniversalFInfinity.RecursiveUniversal.rawAt line 295
  67. def OAI.UniversalFInfinity.RecursiveUniversal.colour line 296
  68. def OAI.UniversalFInfinity.RecursiveUniversal.relator line 297
  69. def OAI.UniversalFInfinity.RecursiveUniversal.allRelations line 298
  70. abbrev OAI.UniversalFInfinity.RecursiveUniversal.Universal line 299
  71. lemma OAI.UniversalFInfinity.RecursiveUniversal.rawAt_encode line 301
  72. lemma OAI.UniversalFInfinity.RecursiveUniversal.coloured_relation line 304
  73. def OAI.UniversalFInfinity.RecursiveUniversal.embed line 311
  74. def OAI.UniversalFInfinity.RecursiveUniversal.project line 316
  75. lemma OAI.UniversalFInfinity.RecursiveUniversal.eval_colour line 319
  76. lemma OAI.UniversalFInfinity.RecursiveUniversal.raw_relation line 328
  77. lemma OAI.UniversalFInfinity.RecursiveUniversal.project_relator line 337
  78. def OAI.UniversalFInfinity.RecursiveUniversal.retract line 350
  79. lemma OAI.UniversalFInfinity.RecursiveUniversal.retract_embed line 353
  80. lemma OAI.UniversalFInfinity.RecursiveUniversal.embed_injective line 360
  81. def OAI.UniversalFInfinity.RecursiveUniversal.rename line 365
  82. def OAI.UniversalFInfinity.RecursiveUniversal.renameValues line 369
  83. lemma OAI.UniversalFInfinity.RecursiveUniversal.renameValues_comp line 372
  84. def OAI.UniversalFInfinity.RecursiveUniversal.renameRetract line 378
  85. lemma OAI.UniversalFInfinity.RecursiveUniversal.renameRetract_comp line 386
  86. lemma OAI.UniversalFInfinity.RecursiveUniversal.rename_injective line 394
  87. lemma OAI.UniversalFInfinity.RecursiveUniversal.code_exists line 400
  88. theorem OAI.UniversalFInfinity.RecursiveUniversal.universal line 413
  89. lemma OAI.UniversalFInfinity.RecursiveUniversal.rawAt_primrec line 424
  90. lemma OAI.UniversalFInfinity.RecursiveUniversal.colour_primrec line 429
  91. theorem OAI.UniversalFInfinity.RecursiveUniversal.relator_primrec line 435
  92. abbrev OAI.UniversalFInfinity.RecursiveUniversalThree.Raw line 444
  93. def OAI.UniversalFInfinity.RecursiveUniversalThree.positive line 446
  94. def OAI.UniversalFInfinity.RecursiveUniversalThree.v line 447
  95. def OAI.UniversalFInfinity.RecursiveUniversalThree.replacement line 448
  96. def OAI.UniversalFInfinity.RecursiveUniversalThree.substituteRaw line 450
  97. def OAI.UniversalFInfinity.RecursiveUniversalThree.enumerator line 452
  98. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.mk_positive line 454
  99. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.mk_v line 462
  100. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.mk_replacement line 466
  101. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.mk_substituteRaw line 472
  102. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.enumerated_relations line 488
  103. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.invRev_primrec line 497
  104. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.positive_primrec line 504
  105. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.v_primrec line 511
  106. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.replacement_primrec line 516
  107. lemma OAI.UniversalFInfinity.RecursiveUniversalThree.substituteRaw_primrec line 521
  108. theorem OAI.UniversalFInfinity.RecursiveUniversalThree.enumerator_primrec line 530
  109. abbrev OAI.UniversalFInfinity.RecursiveUniversalThree.Universal line 533
  110. theorem OAI.UniversalFInfinity.RecursiveUniversalThree.universal line 535
  111. theorem OAI.UniversalFInfinity.exists_universal_finitely_presented line 548