OAI/Algebra/OddKaplansky/Diagrams.lean

GitHub source file

298 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.Planar.Cycles line 23
  2. def OAI.OddKaplansky.Planar.cycleClass line 25
  3. def OAI.OddKaplansky.Planar.cycleSet line 27
  4. lemma OAI.OddKaplansky.Planar.mem_cycleSet line 30
  5. lemma OAI.OddKaplansky.Planar.cycleClass_eq line 34
  6. lemma OAI.OddKaplansky.Planar.cycleSet_nonempty line 37
  7. lemma OAI.OddKaplansky.Planar.cycles_sum_card line 41
  8. structure OAI.OddKaplansky.Planar.Ribbon line 47
  9. def OAI.OddKaplansky.Planar.Ribbon.face line 51
  10. def OAI.OddKaplansky.Planar.Ribbon.Spherical line 53
  11. def OAI.OddKaplansky.Planar.Ribbon.mergeWhite line 57
  12. lemma OAI.OddKaplansky.Planar.mergeWhite_face line 62
  13. lemma OAI.OddKaplansky.Planar.mergeWhite_face_fixed line 67
  14. lemma OAI.OddKaplansky.Planar.sameCycle_map line 71
  15. def OAI.OddKaplansky.Planar.unplug line 82
  16. def OAI.OddKaplansky.Planar.bypass line 84
  17. lemma OAI.OddKaplansky.Planar.unplug_fixed line 87
  18. lemma OAI.OddKaplansky.Planar.unplug_sameCycle line 90
  19. lemma OAI.OddKaplansky.Planar.sameCycle_bypass line 105
  20. lemma OAI.OddKaplansky.Planar.unplug_sameCycle_iff line 126
  21. lemma OAI.OddKaplansky.Planar.bypass_ne line 133
  22. def OAI.OddKaplansky.Planar.unplugCycleEquiv line 137
  23. lemma OAI.OddKaplansky.Planar.unplug_cycles_card line 164
  24. lemma OAI.OddKaplansky.Planar.swap_mul_sameCycle line 173
  25. lemma OAI.OddKaplansky.Planar.sameCycle_swap_mul line 206
  26. def OAI.OddKaplansky.Planar.mergedClass line 222
  27. lemma OAI.OddKaplansky.Planar.cycleClass_apply line 226
  28. lemma OAI.OddKaplansky.Planar.mergedClass_step line 231
  29. lemma OAI.OddKaplansky.Planar.mergedClass_cycle line 245
  30. def OAI.OddKaplansky.Planar.mergeCycleEquiv line 256
  31. lemma OAI.OddKaplansky.Planar.swap_mul_cycles_card line 283
  32. lemma OAI.OddKaplansky.Planar.mergeWhite_spherical line 291
  33. theorem OAI.OddKaplansky.Planar.euler_contradiction line 310
  34. lemma OAI.OddKaplansky.Planar.sameCycle_map_quotient line 333
  35. lemma OAI.OddKaplansky.Planar.swap_cycles_card_le line 339
  36. lemma OAI.OddKaplansky.Planar.cycles_card_le line 365
  37. lemma OAI.OddKaplansky.Planar.cycles_one_card line 368
  38. lemma OAI.OddKaplansky.Planar.exists_cycle_factorization line 375
  39. def OAI.OddKaplansky.Planar.mergeClass line 418
  40. def OAI.OddKaplansky.Planar.joinPair line 421
  41. lemma OAI.OddKaplansky.Planar.le_joinPair line 423
  42. lemma OAI.OddKaplansky.Planar.joinPair_related line 428
  43. lemma OAI.OddKaplansky.Planar.joinPair_eq_of_related line 432
  44. lemma OAI.OddKaplansky.Planar.joinPair_le line 444
  45. def OAI.OddKaplansky.Planar.joinPairEquiv line 459
  46. lemma OAI.OddKaplansky.Planar.joinPair_card line 483
  47. lemma OAI.OddKaplansky.Planar.setoid_swap_related line 491
  48. lemma OAI.OddKaplansky.Planar.setoid_sameCycle_of_step line 501
  49. def OAI.OddKaplansky.Planar.edgePartition line 511
  50. lemma OAI.OddKaplansky.Planar.edgePartition_le line 515
  51. lemma OAI.OddKaplansky.Planar.edgePartition_pair line 523
  52. lemma OAI.OddKaplansky.Planar.edgePartition_prod line 532
  53. lemma OAI.OddKaplansky.Planar.transposition_euler_bound line 541
  54. lemma OAI.OddKaplansky.Planar.quotient_card_antitone line 573
  55. def OAI.OddKaplansky.Planar.Ribbon.components line 578
  56. lemma OAI.OddKaplansky.Planar.cycles_inv_card line 582
  57. theorem OAI.OddKaplansky.Planar.Ribbon.euler_le line 589
  58. def OAI.OddKaplansky.Planar.restrictQuotient line 635
  59. lemma OAI.OddKaplansky.Planar.restrictQuotient_injective line 639
  60. def OAI.OddKaplansky.Planar.quotientRestrictSumEquiv line 650
  61. lemma OAI.OddKaplansky.Planar.quotient_restrict_card_split line 677
  62. lemma OAI.OddKaplansky.Planar.perm_invariant_cycle line 686
  63. lemma OAI.OddKaplansky.Planar.subtype_cycles_setoid line 692
  64. lemma OAI.OddKaplansky.Planar.cycles_restrict_card_split line 698
  65. def OAI.OddKaplansky.Planar.Ribbon.restrict line 705
  66. lemma OAI.OddKaplansky.Planar.Ribbon.restrict_face line 712
  67. lemma OAI.OddKaplansky.Planar.Ribbon.invariant_components line 715
  68. lemma OAI.OddKaplansky.Planar.Ribbon.restrict_components line 724
  69. def OAI.OddKaplansky.Planar.Ribbon.GenusZero line 759
  70. lemma OAI.OddKaplansky.Planar.Ribbon.planar_restrict line 763
  71. lemma OAI.OddKaplansky.Planar.Ribbon.black_step line 797
  72. lemma OAI.OddKaplansky.Planar.Ribbon.white_step line 801
  73. lemma OAI.OddKaplansky.Planar.Ribbon.components_le_of_steps line 804
  74. lemma OAI.OddKaplansky.Planar.Ribbon.black_component_invariant line 810
  75. lemma OAI.OddKaplansky.Planar.Ribbon.white_component_invariant line 817
  76. def OAI.OddKaplansky.Planar.Ribbon.keepComponent line 823
  77. lemma OAI.OddKaplansky.Planar.Ribbon.keepComponent_card line 827
  78. lemma OAI.OddKaplansky.Planar.Ribbon.spherical_keepComponent line 839
  79. lemma OAI.OddKaplansky.Planar.joinPair_left_iff line 849
  80. def OAI.OddKaplansky.Planar.Ribbon.detach line 860
  81. lemma OAI.OddKaplansky.Planar.Ribbon.detach_fixed_black line 865
  82. lemma OAI.OddKaplansky.Planar.Ribbon.detach_fixed_white line 868
  83. lemma OAI.OddKaplansky.Planar.Ribbon.detach_isolated line 871
  84. lemma OAI.OddKaplansky.Planar.Ribbon.detach_components_le line 891
  85. lemma OAI.OddKaplansky.Planar.Ribbon.components_detach line 899
  86. lemma OAI.OddKaplansky.Planar.Ribbon.detach_face line 926
  87. lemma OAI.OddKaplansky.Planar.Ribbon.detach_face_of_face_fixed line 933
  88. lemma OAI.OddKaplansky.Planar.Ribbon.detach_face_unplug line 939
  89. lemma OAI.OddKaplansky.Planar.Ribbon.detach_face_card_le line 946
  90. lemma OAI.OddKaplansky.Planar.Ribbon.face_step line 964
  91. lemma OAI.OddKaplansky.Planar.Ribbon.sameCycle_face_components line 967
  92. lemma OAI.OddKaplansky.Planar.Ribbon.detach_components_card line 970
  93. lemma OAI.OddKaplansky.Planar.Ribbon.detach_components_card_black_fixed line 995
  94. lemma OAI.OddKaplansky.Planar.Ribbon.detach_components_card_white_fixed line 1005
  95. lemma OAI.OddKaplansky.Planar.Ribbon.detach_face_black_fixed line 1016
  96. lemma OAI.OddKaplansky.Planar.Ribbon.detach_face_white_fixed line 1024
  97. lemma OAI.OddKaplansky.Planar.Ribbon.detach_face_card_separating line 1030
  98. theorem OAI.OddKaplansky.Planar.Ribbon.genusZero_detach line 1057
  99. lemma OAI.OddKaplansky.Planar.Ribbon.mergeWhite_components line 1115
  100. lemma OAI.OddKaplansky.Planar.Ribbon.genusZero_mergeWhite line 1130
  101. def OAI.OddKaplansky.Planar.Ribbon.mergeBlack line 1142
  102. lemma OAI.OddKaplansky.Planar.Ribbon.mergeBlack_face line 1147
  103. lemma OAI.OddKaplansky.Planar.Ribbon.mergeBlack_components line 1153
  104. lemma OAI.OddKaplansky.Planar.Ribbon.genusZero_mergeBlack line 1169
  105. lemma OAI.OddKaplansky.Planar.label_swap line 1185
  106. lemma OAI.OddKaplansky.Planar.sameCycle_after_swap line 1201
  107. lemma OAI.OddKaplansky.Planar.sign_eq_cycles line 1208
  108. lemma OAI.OddKaplansky.Planar.not_sameCycle_swap_of_sameCycle line 1220
  109. lemma OAI.OddKaplansky.Planar.swap_mul_cycles_card_split line 1242
  110. def OAI.OddKaplansky.Planar.Ribbon.swapBlack line 1255
  111. lemma OAI.OddKaplansky.Planar.Ribbon.swapBlack_twice line 1259
  112. lemma OAI.OddKaplansky.Planar.Ribbon.swapBlack_face line 1265
  113. lemma OAI.OddKaplansky.Planar.Ribbon.swapBlack_components_merge line 1270
  114. lemma OAI.OddKaplansky.Planar.Ribbon.not_blackCycle_of_not_component line 1293
  115. lemma OAI.OddKaplansky.Planar.Ribbon.not_white_faceCycle_of_not_component line 1297
  116. lemma OAI.OddKaplansky.Planar.Ribbon.genusZero_swapBlack_merge line 1304
  117. lemma OAI.OddKaplansky.Planar.Ribbon.genusZero_swapBlack_split line 1319
  118. structure OAI.OddKaplansky.Planar.NoncommBalanced line 1357
  119. def OAI.OddKaplansky.Planar.NoncommBalanced.Reduced line 1373
  120. lemma OAI.OddKaplansky.Planar.cycleClass_perm line 1379
  121. lemma OAI.OddKaplansky.Planar.cycleSet_singleton_of_fixed line 1385
  122. lemma OAI.OddKaplansky.Planar.cycleSet_card_pow line 1392
  123. lemma OAI.OddKaplansky.Planar.NoncommBalanced.exception_weight_fixed line 1405
  124. lemma OAI.OddKaplansky.Planar.NoncommBalanced.white_not_fixed line 1411
  125. lemma OAI.OddKaplansky.Planar.NoncommBalanced.black_iterate line 1418
  126. structure OAI.OddKaplansky.Holonomy.Defect line 1440
  127. def OAI.OddKaplansky.Holonomy.combineWeight line 1446
  128. def OAI.OddKaplansky.Holonomy.combinePotential line 1448
  129. def OAI.OddKaplansky.Holonomy.Defect.combine line 1451
  130. def OAI.OddKaplansky.Holonomy.Defect.merge line 1510
  131. def OAI.OddKaplansky.Holonomy.Defect.swapEqual line 1541
  132. def OAI.OddKaplansky.Holonomy.Defect.restrict line 1555
  133. def OAI.OddKaplansky.Holonomy.Defect.splitRestrict line 1563
  134. def OAI.OddKaplansky.Holonomy.Defect.unplug line 1592
  135. def OAI.OddKaplansky.Planar.cycleMap line 1656
  136. lemma OAI.OddKaplansky.Planar.cycleMap_class line 1660
  137. lemma OAI.OddKaplansky.Planar.prod_cycle_coarsen line 1663
  138. lemma OAI.OddKaplansky.Planar.prod_cycle_coarsen_one line 1674
  139. lemma OAI.OddKaplansky.Planar.label_sameCycle line 1681
  140. lemma OAI.OddKaplansky.Planar.label_unplug line 1685
  141. lemma OAI.OddKaplansky.Planar.sameCycle_unplug_iff_of_ne line 1689
  142. lemma OAI.OddKaplansky.Planar.cycleSet_unplug line 1696
  143. lemma OAI.OddKaplansky.Planar.prod_erase_of_one line 1712
  144. lemma OAI.OddKaplansky.Planar.prod_cycle_unplug line 1720
  145. def OAI.OddKaplansky.Planar.cycleSubtypeMap line 1727
  146. lemma OAI.OddKaplansky.Planar.cycleSubtypeMap_injective line 1732
  147. lemma OAI.OddKaplansky.Planar.prod_cycle_subtype line 1742
  148. lemma OAI.OddKaplansky.Planar.prod_combineWeight line 1765
  149. def OAI.OddKaplansky.Planar.NoncommBalanced.localWeight line 1784
  150. def OAI.OddKaplansky.Planar.NoncommBalanced.defect line 1787
  151. def OAI.OddKaplansky.Planar.NoncommBalanced.withDefect line 1790
  152. def OAI.OddKaplansky.Planar.NoncommBalanced.combine line 1802
  153. def OAI.OddKaplansky.Planar.NoncommBalanced.restrict line 1824
  154. def OAI.OddKaplansky.Planar.NoncommBalanced.detach line 1842
  155. def OAI.OddKaplansky.Planar.NoncommBalanced.mergeWhite line 1871
  156. def OAI.OddKaplansky.Planar.NoncommBalanced.spliceBlack line 1886
  157. lemma OAI.OddKaplansky.Planar.fixed_compl_invariant line 1901
  158. lemma OAI.OddKaplansky.Planar.NoncommBalanced.exists_smaller line 1907
  159. lemma OAI.OddKaplansky.Planar.Ribbon.mergeBlack_separates line 1931
  160. structure OAI.OddKaplansky.Planar.ShortWords line 1964
  161. lemma OAI.OddKaplansky.Planar.NoncommBalanced.black_fixed_exception line 1974
  162. lemma OAI.OddKaplansky.Planar.NoncommBalanced.cycle_product_eq_one line 1983
  163. lemma OAI.OddKaplansky.Planar.NoncommBalanced.black_degree line 1993
  164. lemma OAI.OddKaplansky.Planar.NoncommBalanced.white_degree line 2052
  165. def OAI.OddKaplansky.Planar.incidenceGraph line 2068
  166. def OAI.OddKaplansky.Planar.NoncommBalanced.exceptionFace line 2078
  167. lemma OAI.OddKaplansky.Planar.NoncommBalanced.black_not_fixed_on_other_face line 2081
  168. def OAI.OddKaplansky.Planar.NoncommBalanced.halfStep line 2089
  169. lemma OAI.OddKaplansky.Planar.NoncommBalanced.halfStep_length line 2096
  170. def OAI.OddKaplansky.Planar.NoncommBalanced.boundary line 2099
  171. lemma OAI.OddKaplansky.Planar.NoncommBalanced.boundary_length line 2106
  172. lemma OAI.OddKaplansky.Planar.NoncommBalanced.boundary_getVert_even line 2115
  173. lemma OAI.OddKaplansky.Planar.NoncommBalanced.boundary_getVert_odd line 2133
  174. lemma OAI.OddKaplansky.Planar.cycleClass_pow line 2150
  175. lemma OAI.OddKaplansky.Planar.NoncommBalanced.boundary_reduced line 2154
  176. lemma OAI.OddKaplansky.Planar.NoncommBalanced.face_degree line 2186
  177. theorem OAI.OddKaplansky.Planar.NoncommBalanced.reduced_not_genusZero line 2218
  178. def OAI.OddKaplansky.Planar.NoncommBalanced.spliceRestrict line 2247
  179. lemma OAI.OddKaplansky.Planar.NoncommBalanced.exists_smaller_of_split line 2270
  180. def OAI.OddKaplansky.Planar.NoncommBalanced.Minimal line 2309
  181. lemma OAI.OddKaplansky.Planar.NoncommBalanced.minimal_no_one line 2314
  182. lemma OAI.OddKaplansky.Planar.NoncommBalanced.minimal_black_reduced line 2320
  183. lemma OAI.OddKaplansky.Planar.NoncommBalanced.minimal_white_reduced line 2340
  184. lemma OAI.OddKaplansky.Planar.NoncommBalanced.minimal_reduced line 2374
  185. theorem OAI.OddKaplansky.Planar.NoncommBalanced.not_genusZero line 2378
  186. def OAI.OddKaplansky.Planar.sumSetoid line 2401
  187. lemma OAI.OddKaplansky.Planar.sumSetoid_inl line 2404
  188. lemma OAI.OddKaplansky.Planar.sumSetoid_inr line 2409
  189. lemma OAI.OddKaplansky.Planar.sumSetoid_cross line 2414
  190. def OAI.OddKaplansky.Planar.sumSetoidEquiv line 2419
  191. lemma OAI.OddKaplansky.Planar.sumSetoid_card line 2428
  192. lemma OAI.OddKaplansky.Planar.sumSetoid_le line 2432
  193. lemma OAI.OddKaplansky.Planar.sumCongr_cycles_setoid line 2443
  194. lemma OAI.OddKaplansky.Planar.sumCongr_cycles_card line 2460
  195. def OAI.OddKaplansky.Planar.Ribbon.sum line 2465
  196. lemma OAI.OddKaplansky.Planar.Ribbon.sum_face line 2469
  197. lemma OAI.OddKaplansky.Planar.Ribbon.sum_components line 2474
  198. lemma OAI.OddKaplansky.Planar.Ribbon.genusZero_sum line 2494
  199. lemma OAI.OddKaplansky.Planar.formPerm_append_nonempty line 2504
  200. def OAI.OddKaplansky.Planar.Ribbon.wheel line 2526
  201. def OAI.OddKaplansky.Planar.sumIndex line 2529
  202. def OAI.OddKaplansky.Planar.wheelFaceIndex line 2531
  203. lemma OAI.OddKaplansky.Planar.wheel_white_index line 2534
  204. lemma OAI.OddKaplansky.Planar.wheel_face_index line 2538
  205. lemma OAI.OddKaplansky.Planar.wheel_white_setoid line 2542
  206. lemma OAI.OddKaplansky.Planar.wheel_face_setoid line 2554
  207. lemma OAI.OddKaplansky.Planar.wheel_component_index line 2578
  208. lemma OAI.OddKaplansky.Planar.wheel_white_card line 2606
  209. lemma OAI.OddKaplansky.Planar.wheel_face_card line 2612
  210. lemma OAI.OddKaplansky.Planar.wheel_component_card line 2618
  211. lemma OAI.OddKaplansky.Planar.Ribbon.genusZero_wheel line 2627
  212. def OAI.OddKaplansky.Planar.Follows line 2640
  213. lemma OAI.OddKaplansky.Planar.Follows.invariant line 2643
  214. lemma OAI.OddKaplansky.Planar.Follows.sameCycle line 2658
  215. lemma OAI.OddKaplansky.Planar.Follows.cycleSet line 2669
  216. lemma OAI.OddKaplansky.Planar.sameCycle_iff_of_eqOn_cycle line 2680
  217. lemma OAI.OddKaplansky.Planar.cycleSet_eq_of_eqOn_cycle line 2699
  218. lemma OAI.OddKaplansky.Planar.formPerm_map_apply line 2707
  219. lemma OAI.OddKaplansky.Planar.Follows.map_sum_left line 2722
  220. lemma OAI.OddKaplansky.Planar.sumCongr_sameCycle_inl line 2736
  221. lemma OAI.OddKaplansky.Planar.sumCongr_sameCycle_inr line 2742
  222. lemma OAI.OddKaplansky.Planar.sumCongr_not_sameCycle line 2748
  223. lemma OAI.OddKaplansky.Planar.prod_cycle_sum_left line 2754
  224. lemma OAI.OddKaplansky.Planar.prod_cycle_sum_right line 2761
  225. def OAI.OddKaplansky.Planar.cycleInl line 2768
  226. lemma OAI.OddKaplansky.Planar.cycleInl_class line 2771
  227. lemma OAI.OddKaplansky.Planar.cycleInl_injective line 2774
  228. lemma OAI.OddKaplansky.Planar.cycleInl_ne_inr line 2785
  229. lemma OAI.OddKaplansky.Planar.Follows.append_rotate line 2798
  230. lemma OAI.OddKaplansky.Planar.Follows.split line 2804
  231. lemma OAI.OddKaplansky.Planar.Follows.map_sum_right line 2831
  232. lemma OAI.OddKaplansky.Planar.Follows.merge line 2839
  233. lemma OAI.OddKaplansky.Planar.follows_formPerm line 2860
  234. def OAI.OddKaplansky.Planar.listPotential line 2871
  235. lemma OAI.OddKaplansky.Planar.listPotential_get line 2874
  236. lemma OAI.OddKaplansky.Planar.listPrefix_succ line 2879
  237. lemma OAI.OddKaplansky.Planar.listPotential_balance_at line 2884
  238. lemma OAI.OddKaplansky.Planar.listPotential_end_at line 2890
  239. lemma OAI.OddKaplansky.Planar.listPotential_balance line 2902
  240. def OAI.OddKaplansky.Planar.listDefect line 2911
  241. def OAI.OddKaplansky.Planar.augInc line 2937
  242. def OAI.OddKaplansky.Planar.augMap line 2941
  243. structure OAI.OddKaplansky.Planar.OpenBalanced line 2945
  244. structure OAI.OddKaplansky.Planar.FlatOpenBalanced line 2950
  245. def OAI.OddKaplansky.Planar.OpenBalanced.sumZero line 2965
  246. def OAI.OddKaplansky.Planar.OpenBalanced.joinNone line 2996
  247. def OAI.OddKaplansky.Planar.OpenBalanced.fill line 3005
  248. structure OAI.OddKaplansky.Planar.OpenDiagram line 3050
  249. def OAI.OddKaplansky.Planar.OpenDiagram.close line 3069
  250. theorem OAI.OddKaplansky.Planar.OpenDiagram.not_empty line 3105
  251. lemma OAI.OddKaplansky.Planar.cycleSet_wheel_white line 3116
  252. def OAI.OddKaplansky.Planar.FlatOpenBalanced.wheel line 3127
  253. def OAI.OddKaplansky.Planar.OpenBalanced.wheel line 3151
  254. def OAI.OddKaplansky.Planar.wordWheel line 3186
  255. def OAI.OddKaplansky.Planar.OpenDiagram.initial line 3199
  256. theorem OAI.OddKaplansky.Planar.OpenDiagram.deleteBlock line 3261
  257. theorem OAI.OddKaplansky.Planar.OpenDiagram.insertBlock line 3347
  258. theorem OAI.OddKaplansky.Planar.OpenDiagram.deleteWordBlock line 3462
  259. theorem OAI.OddKaplansky.Planar.OpenDiagram.insertWordBlock line 3492
  260. abbrev OAI.OddKaplansky.WordReduction.Word line 3506
  261. inductive OAI.OddKaplansky.WordReduction.Delete line 3508
  262. abbrev OAI.OddKaplansky.WordReduction.Related line 3512
  263. lemma OAI.OddKaplansky.WordReduction.rel_trans line 3516
  264. lemma OAI.OddKaplansky.WordReduction.rel_symm line 3519
  265. lemma OAI.OddKaplansky.WordReduction.Related.append_left line 3522
  266. lemma OAI.OddKaplansky.WordReduction.Related.append_right line 3533
  267. lemma OAI.OddKaplansky.WordReduction.Related.inv line 3544
  268. lemma OAI.OddKaplansky.WordReduction.related_of_red_step line 3558
  269. lemma OAI.OddKaplansky.WordReduction.related_of_red line 3565
  270. lemma OAI.OddKaplansky.WordReduction.related_of_mk_eq line 3572
  271. lemma OAI.OddKaplansky.WordReduction.related_append_null line 3578
  272. def OAI.OddKaplansky.WordReduction.nullSubgroup line 3582
  273. lemma OAI.OddKaplansky.WordReduction.nullSubgroup_normal line 3593
  274. theorem OAI.OddKaplansky.WordReduction.of_presented_eq_one line 3611
  275. theorem OAI.OddKaplansky.Planar.OpenDiagram.related_iff line 3634
  276. abbrev OAI.OddKaplansky.GluedGroup.Generator line 3664
  277. abbrev OAI.OddKaplansky.GluedGroup.LocalGenerator line 3665
  278. def OAI.OddKaplansky.GluedGroup.includeLocal line 3667
  279. def OAI.OddKaplansky.GluedGroup.localEvaluation line 3670
  280. def OAI.OddKaplansky.GluedGroup.relators line 3673
  281. abbrev OAI.OddKaplansky.GluedGroup.N line 3677
  282. def OAI.OddKaplansky.GluedGroup.fromLocal line 3679
  283. lemma OAI.OddKaplansky.GluedGroup.local_kernel_le line 3682
  284. def OAI.OddKaplansky.GluedGroup.signedToken line 3686
  285. def OAI.OddKaplansky.GluedGroup.Allowed line 3689
  286. lemma OAI.OddKaplansky.GluedGroup.signedToken_inv line 3693
  287. lemma OAI.OddKaplansky.GluedGroup.allowed_inv line 3698
  288. lemma OAI.OddKaplansky.GluedGroup.allowed_cancel line 3720
  289. lemma OAI.OddKaplansky.GluedGroup.localEvaluation_word line 3730
  290. lemma OAI.OddKaplansky.GluedGroup.relators_allowed line 3741
  291. theorem OAI.OddKaplansky.GluedGroup.fromLocal_eq_one_iff line 3755
  292. abbrev OAI.OddKaplansky.GluedGroup.Local line 3787
  293. def OAI.OddKaplansky.GluedGroup.theta line 3789
  294. lemma OAI.OddKaplansky.GluedGroup.theta_evaluation line 3797
  295. theorem OAI.OddKaplansky.GluedGroup.theta_injective line 3801
  296. def OAI.OddKaplansky.GluedGroup.localEdge line 3821
  297. lemma OAI.OddKaplansky.GluedGroup.localEdge_val line 3824
  298. lemma OAI.OddKaplansky.GluedGroup.theta_localEdge line 3829