OAI/Algebra/Drinfeld/Ordering.lean

GitHub source file

445 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.WordGrading.algHom_homogeneous line 13
  2. theorem OAI.DeligneDrinfeld.WordGrading.algHom_above line 29
  3. theorem OAI.DeligneDrinfeld.WordGrading.algHom_below line 43
  4. def OAI.DeligneDrinfeld.PolynomialOrdering.merge line 63
  5. theorem OAI.DeligneDrinfeld.PolynomialOrdering.merge_tmul line 65
  6. def OAI.DeligneDrinfeld.PolynomialOrdering.ordered line 68
  7. theorem OAI.DeligneDrinfeld.PolynomialOrdering.normalize_merge line 71
  8. theorem OAI.DeligneDrinfeld.PolynomialOrdering.merge_injective line 79
  9. theorem OAI.DeligneDrinfeld.PolynomialOrdering.fiberIn_homogeneous line 83
  10. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseIn_homogeneous line 91
  11. theorem OAI.DeligneDrinfeld.PolynomialOrdering.merge_word_homogeneous line 99
  12. theorem OAI.DeligneDrinfeld.PolynomialOrdering.merge_homogeneous line 104
  13. theorem OAI.DeligneDrinfeld.PolynomialOrdering.merge_above line 110
  14. theorem OAI.DeligneDrinfeld.PolynomialOrdering.merge_strictlyBelow line 117
  15. theorem OAI.DeligneDrinfeld.PolynomialOrdering.ordered_comparison_above line 125
  16. theorem OAI.DeligneDrinfeld.PolynomialOrdering.ordered_comparison_below line 134
  17. theorem OAI.DeligneDrinfeld.PolynomialOrdering.normalize_homogeneous line 142
  18. theorem OAI.DeligneDrinfeld.PolynomialOrdering.normalize_above line 159
  19. theorem OAI.DeligneDrinfeld.PolynomialOrdering.normalize_strictlyBelow line 175
  20. def OAI.DeligneDrinfeld.PolynomialOrdering.baseStage line 191
  21. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseStage_tmul line 193
  22. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseStage_homogeneous line 196
  23. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseIn_above line 206
  24. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseIn_strictlyBelow line 212
  25. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseStage_above line 219
  26. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseStage_strictlyBelow line 229
  27. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseStage_difference_above line 242
  28. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseStage_difference_below line 255
  29. def OAI.DeligneDrinfeld.PolynomialOrdering.iterated line 268
  30. theorem OAI.DeligneDrinfeld.PolynomialOrdering.iterated_comparison_above line 271
  31. theorem OAI.DeligneDrinfeld.PolynomialOrdering.iterated_comparison_below line 293
  32. theorem OAI.DeligneDrinfeld.PolynomialOrdering.iterated_above line 315
  33. theorem OAI.DeligneDrinfeld.WordGrading.eq_zero_of_homogeneous_above line 326
  34. theorem OAI.DeligneDrinfeld.WordGrading.count_transfer line 335
  35. def OAI.DeligneDrinfeld.AlphabetTransport.map line 357
  36. theorem OAI.DeligneDrinfeld.AlphabetTransport.map_atom line 358
  37. theorem OAI.DeligneDrinfeld.AlphabetTransport.map_inverse line 359
  38. theorem OAI.DeligneDrinfeld.AlphabetTransport.map_homogeneous line 366
  39. theorem OAI.DeligneDrinfeld.AlphabetTransport.map_above line 374
  40. theorem OAI.DeligneDrinfeld.AlphabetTransport.map_below line 382
  41. theorem OAI.DeligneDrinfeld.AlphabetTransport.map_strictlyBelow line 390
  42. abbrev OAI.DeligneDrinfeld.SecondStage.K line 401
  43. abbrev OAI.DeligneDrinfeld.SecondStage.F line 402
  44. abbrev OAI.DeligneDrinfeld.SecondStage.B line 403
  45. abbrev OAI.DeligneDrinfeld.SecondStage.E line 404
  46. abbrev OAI.DeligneDrinfeld.SecondStage.Old line 405
  47. def OAI.DeligneDrinfeld.SecondStage.toOld line 407
  48. def OAI.DeligneDrinfeld.SecondStage.fromOld line 408
  49. def OAI.DeligneDrinfeld.SecondStage.equiv line 409
  50. def OAI.DeligneDrinfeld.SecondStage.fc line 417
  51. def OAI.DeligneDrinfeld.SecondStage.bc line 418
  52. def OAI.DeligneDrinfeld.SecondStage.count line 419
  53. theorem OAI.DeligneDrinfeld.SecondStage.count_toOld line 421
  54. theorem OAI.DeligneDrinfeld.SecondStage.count_fromOld line 426
  55. def OAI.DeligneDrinfeld.SecondStage.outward line 429
  56. def OAI.DeligneDrinfeld.SecondStage.inward line 430
  57. theorem OAI.DeligneDrinfeld.SecondStage.outward_inward line 431
  58. theorem OAI.DeligneDrinfeld.SecondStage.inward_outward line 433
  59. def OAI.DeligneDrinfeld.SecondStage.H line 436
  60. def OAI.DeligneDrinfeld.SecondStage.U line 437
  61. def OAI.DeligneDrinfeld.SecondStage.V line 438
  62. abbrev OAI.DeligneDrinfeld.SecondStage.bracket line 439
  63. def OAI.DeligneDrinfeld.SecondStage.common line 440
  64. def OAI.DeligneDrinfeld.SecondStage.higher line 443
  65. def OAI.DeligneDrinfeld.SecondStage.source line 447
  66. theorem OAI.DeligneDrinfeld.SecondStage.H_homo line 449
  67. theorem OAI.DeligneDrinfeld.SecondStage.U_homo line 450
  68. theorem OAI.DeligneDrinfeld.SecondStage.V_homo line 451
  69. theorem OAI.DeligneDrinfeld.SecondStage.bracket_homo line 452
  70. theorem OAI.DeligneDrinfeld.SecondStage.common_homo line 458
  71. theorem OAI.DeligneDrinfeld.SecondStage.higher_homo line 464
  72. theorem OAI.DeligneDrinfeld.SecondStage.source_above line 472
  73. theorem OAI.DeligneDrinfeld.SecondStage.source_difference line 475
  74. def OAI.DeligneDrinfeld.SecondStage.order line 479
  75. theorem OAI.DeligneDrinfeld.SecondStage.order_common_homogeneous line 482
  76. theorem OAI.DeligneDrinfeld.SecondStage.order_source_above line 489
  77. theorem OAI.DeligneDrinfeld.SecondStage.order_difference line 496
  78. theorem OAI.DeligneDrinfeld.SecondStage.order_common_below line 505
  79. abbrev OAI.DeligneDrinfeld.ExactCountOrdering.K line 515
  80. abbrev OAI.DeligneDrinfeld.ExactCountOrdering.E line 516
  81. def OAI.DeligneDrinfeld.ExactCountOrdering.count line 517
  82. def OAI.DeligneDrinfeld.ExactCountOrdering.S line 518
  83. def OAI.DeligneDrinfeld.ExactCountOrdering.C line 519
  84. def OAI.DeligneDrinfeld.ExactCountOrdering.T line 520
  85. theorem OAI.DeligneDrinfeld.ExactCountOrdering.source_comparison line 522
  86. theorem OAI.DeligneDrinfeld.ExactCountOrdering.target_comparison line 528
  87. theorem OAI.DeligneDrinfeld.ExactCountOrdering.source_above line 537
  88. theorem OAI.DeligneDrinfeld.ExactCountOrdering.transfer line 541
  89. theorem OAI.DeligneDrinfeld.PolynomialOrdering.evaluate_fiber line 554
  90. theorem OAI.DeligneDrinfeld.PolynomialOrdering.evaluate_base line 561
  91. theorem OAI.DeligneDrinfeld.PolynomialOrdering.evaluate_merge line 568
  92. theorem OAI.DeligneDrinfeld.PolynomialOrdering.evaluate_ordered line 576
  93. theorem OAI.DeligneDrinfeld.PolynomialOrdering.evaluate_baseStage line 582
  94. theorem OAI.DeligneDrinfeld.PolynomialOrdering.evaluate_iterated line 591
  95. abbrev OAI.DeligneDrinfeld.SourceEnveloping.K line 603
  96. abbrev OAI.DeligneDrinfeld.SourceEnveloping.Env line 604
  97. def OAI.DeligneDrinfeld.SourceEnveloping.augment line 607
  98. instance OAI.DeligneDrinfeld.SourceEnveloping.envCharP line 608
  99. theorem OAI.DeligneDrinfeld.SourceEnveloping.fiberIn_injective line 614
  100. theorem OAI.DeligneDrinfeld.SourceEnveloping.fiberIn_atom line 625
  101. theorem OAI.DeligneDrinfeld.SourceEnveloping.baseIn_ι line 630
  102. def OAI.DeligneDrinfeld.SourceEnveloping.chord line 635
  103. theorem OAI.DeligneDrinfeld.SourceEnveloping.chord_self line 636
  104. theorem OAI.DeligneDrinfeld.SourceEnveloping.chord_comm line 637
  105. theorem OAI.DeligneDrinfeld.SourceEnveloping.base_chord line 640
  106. theorem OAI.DeligneDrinfeld.SourceEnveloping.fiber_chord line 646
  107. theorem OAI.DeligneDrinfeld.SourceEnveloping.base_fiber_left line 649
  108. theorem OAI.DeligneDrinfeld.SourceEnveloping.base_fiber_right line 654
  109. theorem OAI.DeligneDrinfeld.SourceEnveloping.base_fiber_other line 660
  110. theorem OAI.DeligneDrinfeld.AssociativeAction.of_atoms line 672
  111. abbrev OAI.DeligneDrinfeld.SourceAlphabet.K line 691
  112. theorem OAI.DeligneDrinfeld.SourceAlphabet.map_cancel line 693
  113. theorem OAI.DeligneDrinfeld.SourceAlphabet.map_injective line 701
  114. def OAI.DeligneDrinfeld.SourceAlphabet.letter5 line 705
  115. def OAI.DeligneDrinfeld.SourceAlphabet.letter3 line 714
  116. theorem OAI.DeligneDrinfeld.SourceAlphabet.realize_factor line 722
  117. theorem OAI.DeligneDrinfeld.SourceAlphabet.realize_injective line 731
  118. abbrev OAI.DeligneDrinfeld.SourceModel.K line 744
  119. abbrev OAI.DeligneDrinfeld.SourceModel.S1 line 745
  120. abbrev OAI.DeligneDrinfeld.SourceModel.S2 line 746
  121. abbrev OAI.DeligneDrinfeld.SourceModel.S3 line 747
  122. def OAI.DeligneDrinfeld.SourceModel.swap line 749
  123. def OAI.DeligneDrinfeld.SourceModel.smallLetters line 755
  124. def OAI.DeligneDrinfeld.SourceModel.secondRealize line 761
  125. theorem OAI.DeligneDrinfeld.SourceModel.secondRealize_injective line 763
  126. def OAI.DeligneDrinfeld.SourceModel.square line 768
  127. theorem OAI.DeligneDrinfeld.SourceModel.square_injective line 769
  128. def OAI.DeligneDrinfeld.SourceModel.tail line 785
  129. theorem OAI.DeligneDrinfeld.SourceModel.tail_injective line 786
  130. def OAI.DeligneDrinfeld.SourceModel.secondFiber line 788
  131. def OAI.DeligneDrinfeld.SourceModel.secondBase line 789
  132. def OAI.DeligneDrinfeld.SourceModel.secondNormal line 791
  133. theorem OAI.DeligneDrinfeld.SourceModel.secondNormal_tmul line 793
  134. theorem OAI.DeligneDrinfeld.SourceModel.secondNormal_injective line 796
  135. def OAI.DeligneDrinfeld.SourceModel.topLetters line 800
  136. def OAI.DeligneDrinfeld.SourceModel.topRealize line 808
  137. def OAI.DeligneDrinfeld.SourceModel.topFiber line 811
  138. def OAI.DeligneDrinfeld.SourceModel.tripleNormal line 813
  139. theorem OAI.DeligneDrinfeld.SourceModel.tripleNormal_injective line 816
  140. theorem OAI.DeligneDrinfeld.CharTwoAction.symm line 827
  141. theorem OAI.DeligneDrinfeld.CharTwoAction.square line 829
  142. def OAI.DeligneDrinfeld.SourceModel.root line 842
  143. def OAI.DeligneDrinfeld.SourceModel.one line 843
  144. def OAI.DeligneDrinfeld.SourceModel.two line 844
  145. def OAI.DeligneDrinfeld.SourceModel.oldX line 845
  146. def OAI.DeligneDrinfeld.SourceModel.oldU line 846
  147. def OAI.DeligneDrinfeld.SourceModel.rawFiber line 848
  148. def OAI.DeligneDrinfeld.SourceModel.baseX line 850
  149. def OAI.DeligneDrinfeld.SourceModel.baseU line 851
  150. theorem OAI.DeligneDrinfeld.SourceModel.rawFiber_atom line 853
  151. theorem OAI.DeligneDrinfeld.SourceModel.rawFiber_X line 858
  152. theorem OAI.DeligneDrinfeld.SourceModel.rawFiber_Y line 860
  153. theorem OAI.DeligneDrinfeld.SourceModel.rawFiber_C line 863
  154. theorem OAI.DeligneDrinfeld.SourceModel.baseX_zero line 867
  155. theorem OAI.DeligneDrinfeld.SourceModel.baseX_one line 868
  156. theorem OAI.DeligneDrinfeld.SourceModel.baseU_eq line 869
  157. theorem OAI.DeligneDrinfeld.SourceModel.raw_delta_atoms line 871
  158. theorem OAI.DeligneDrinfeld.SourceModel.raw_delta line 882
  159. theorem OAI.DeligneDrinfeld.SourceModel.raw_epsilon_atoms line 887
  160. theorem OAI.DeligneDrinfeld.SourceModel.raw_epsilon line 895
  161. def OAI.DeligneDrinfeld.SourceModel.oldBase line 900
  162. def OAI.DeligneDrinfeld.SourceModel.topBase line 905
  163. theorem OAI.DeligneDrinfeld.SourceModel.baseDeriv_action line 907
  164. theorem OAI.DeligneDrinfeld.SourceModel.topFiber_eq line 925
  165. theorem OAI.DeligneDrinfeld.SourceModel.top_action line 927
  166. def OAI.DeligneDrinfeld.SourceModel.smallX line 939
  167. def OAI.DeligneDrinfeld.SourceModel.smallY line 940
  168. def OAI.DeligneDrinfeld.SourceModel.smallD line 941
  169. def OAI.DeligneDrinfeld.SourceModel.squash line 942
  170. theorem OAI.DeligneDrinfeld.SourceModel.squash_delta line 945
  171. def OAI.DeligneDrinfeld.SourceModel.smallIndex line 960
  172. theorem OAI.DeligneDrinfeld.SourceModel.secondRealize_factor line 962
  173. theorem OAI.DeligneDrinfeld.SourceModel.small_source line 971
  174. theorem OAI.DeligneDrinfeld.SourceModel.second_realization line 978
  175. def OAI.DeligneDrinfeld.SourceModel.smallRaw line 986
  176. def OAI.DeligneDrinfeld.SourceModel.smallBase line 987
  177. theorem OAI.DeligneDrinfeld.SourceModel.small_action line 989
  178. theorem OAI.DeligneDrinfeld.SourceModel.secondBase_atom line 1003
  179. theorem OAI.DeligneDrinfeld.SourceModel.second_action line 1007
  180. theorem OAI.DeligneDrinfeld.SourceModel.secondFiber_H line 1017
  181. theorem OAI.DeligneDrinfeld.SourceModel.secondFiber_U line 1022
  182. theorem OAI.DeligneDrinfeld.SourceModel.secondFiber_V line 1026
  183. theorem OAI.DeligneDrinfeld.SourceModel.oldX_zero line 1032
  184. theorem OAI.DeligneDrinfeld.SourceModel.oldX_one line 1034
  185. theorem OAI.DeligneDrinfeld.SourceModel.oldU_eq line 1036
  186. theorem OAI.DeligneDrinfeld.SourceModel.oldBase_factor line 1039
  187. def OAI.DeligneDrinfeld.SourceModel.normal2 line 1052
  188. theorem OAI.DeligneDrinfeld.SourceModel.normal2_correct line 1055
  189. def OAI.DeligneDrinfeld.SourceModel.normal3 line 1065
  190. theorem OAI.DeligneDrinfeld.SourceModel.tripleNormal_tmul line 1069
  191. theorem OAI.DeligneDrinfeld.SourceModel.normal3_correct line 1073
  192. def OAI.DeligneDrinfeld.SourceModel.collect2 line 1084
  193. def OAI.DeligneDrinfeld.SourceModel.collect3 line 1087
  194. theorem OAI.DeligneDrinfeld.SourceModel.collect2_normal2 line 1090
  195. theorem OAI.DeligneDrinfeld.SourceModel.collect3_normal3 line 1093
  196. theorem OAI.DeligneDrinfeld.SourceModel.source_zero line 1102
  197. theorem OAI.DeligneDrinfeld.WeightedDeletion.Step.sublist line 1116
  198. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_above line 1122
  199. def OAI.DeligneDrinfeld.WeightedDeletion.action line 1138
  200. theorem OAI.DeligneDrinfeld.WeightedDeletion.action_atom line 1140
  201. theorem OAI.DeligneDrinfeld.WeightedDeletion.action_word_above line 1143
  202. theorem OAI.DeligneDrinfeld.WeightedDeletion.test_word_zero line 1155
  203. theorem OAI.DeligneDrinfeld.WeightedDeletion.linear_ext line 1168
  204. theorem OAI.DeligneDrinfeld.WeightedDeletion.raw_sub line 1177
  205. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_sub line 1183
  206. def OAI.DeligneDrinfeld.WeightedDeletion.cut line 1190
  207. theorem OAI.DeligneDrinfeld.WeightedDeletion.cut_bound line 1193
  208. theorem OAI.DeligneDrinfeld.WeightedDeletion.diff_bound line 1198
  209. theorem OAI.DeligneDrinfeld.WeightedDeletion.Step.count_eq line 1206
  210. theorem OAI.DeligneDrinfeld.WeightedDeletion.Step.count_strict line 1213
  211. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_homogeneous line 1220
  212. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_strict line 1236
  213. theorem OAI.DeligneDrinfeld.WeightedDeletion.exact_allocation line 1253
  214. theorem OAI.DeligneDrinfeld.WeightedDeletion.exact_allocation_test line 1291
  215. abbrev OAI.DeligneDrinfeld.RowTwo.K line 1302
  216. inductive OAI.DeligneDrinfeld.RowTwo.Letter line 1303
  217. instance OAI.DeligneDrinfeld.RowTwo.(instance at line 1304) line 1304
  218. inductive OAI.DeligneDrinfeld.RowTwo.Slot line 1305
  219. instance OAI.DeligneDrinfeld.RowTwo.(instance at line 1306) line 1306
  220. def OAI.DeligneDrinfeld.RowTwo.κ line 1309
  221. def OAI.DeligneDrinfeld.RowTwo.Good line 1314
  222. theorem OAI.DeligneDrinfeld.RowTwo.head_character line 1316
  223. theorem OAI.DeligneDrinfeld.RowTwo.head_good line 1319
  224. theorem OAI.DeligneDrinfeld.RowTwo.step_good line 1350
  225. theorem OAI.DeligneDrinfeld.RowTwo.step_bad line 1366
  226. def OAI.DeligneDrinfeld.RowTwo.badSpace line 1370
  227. theorem OAI.DeligneDrinfeld.RowTwo.op_bad line 1373
  228. theorem OAI.DeligneDrinfeld.RowTwo.word_action_bad line 1385
  229. theorem OAI.DeligneDrinfeld.RowTwo.action_bad line 1393
  230. theorem OAI.DeligneDrinfeld.RowTwo.test_zero line 1402
  231. theorem OAI.DeligneDrinfeld.WeightedDeletion.Step.count_lower line 1416
  232. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_count_lower line 1423
  233. theorem OAI.DeligneDrinfeld.WeightedDeletion.action_count_lower line 1438
  234. theorem OAI.DeligneDrinfeld.WeightedDeletion.test_excess_cost line 1449
  235. def OAI.DeligneDrinfeld.TerminalDeletion.κ line 1464
  236. theorem OAI.DeligneDrinfeld.TerminalDeletion.raw_snoc line 1466
  237. theorem OAI.DeligneDrinfeld.TerminalDeletion.scalar_word line 1481
  238. theorem OAI.DeligneDrinfeld.TerminalDeletion.test line 1519
  239. def OAI.DeligneDrinfeld.Deletion.commSum line 1538
  240. theorem OAI.DeligneDrinfeld.Deletion.commSum_apply line 1542
  241. theorem OAI.DeligneDrinfeld.Deletion.commSum_cons line 1553
  242. theorem OAI.DeligneDrinfeld.Deletion.commSum_eq_zero line 1567
  243. abbrev OAI.DeligneDrinfeld.TargetDeletion.K line 1589
  244. abbrev OAI.DeligneDrinfeld.TargetDeletion.F line 1590
  245. abbrev OAI.DeligneDrinfeld.TargetDeletion.B line 1591
  246. abbrev OAI.DeligneDrinfeld.TargetDeletion.E line 1592
  247. def OAI.DeligneDrinfeld.TargetDeletion.fiber line 1594
  248. def OAI.DeligneDrinfeld.TargetDeletion.base line 1600
  249. def OAI.DeligneDrinfeld.TargetDeletion.labels line 1605
  250. def OAI.DeligneDrinfeld.TargetDeletion.ν line 1607
  251. def OAI.DeligneDrinfeld.TargetDeletion.extra line 1609
  252. def OAI.DeligneDrinfeld.TargetDeletion.pairs line 1621
  253. theorem OAI.DeligneDrinfeld.TargetDeletion.table_curvature line 1624
  254. theorem OAI.DeligneDrinfeld.TargetDeletion.target_eq line 1629
  255. def OAI.DeligneDrinfeld.TargetDeletion.evalFiber line 1639
  256. def OAI.DeligneDrinfeld.TargetDeletion.evalBase line 1641
  257. theorem OAI.DeligneDrinfeld.TargetDeletion.evalFiber_atom line 1644
  258. theorem OAI.DeligneDrinfeld.TargetDeletion.evalBase_atom line 1646
  259. theorem OAI.DeligneDrinfeld.TargetDeletion.sum_extra line 1649
  260. theorem OAI.DeligneDrinfeld.TargetDeletion.action_table line 1658
  261. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_count_exact line 1678
  262. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_count_lt line 1693
  263. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_count_lt_of_exact line 1708
  264. theorem OAI.DeligneDrinfeld.WeightedDeletion.diff_lower_bound line 1723
  265. theorem OAI.DeligneDrinfeld.WeightedDeletion.exact_allocation_lower line 1731
  266. theorem OAI.DeligneDrinfeld.WeightedDeletion.exact_allocation_lower_test line 1767
  267. def OAI.DeligneDrinfeld.WeightedDeletion.scalar line 1775
  268. theorem OAI.DeligneDrinfeld.WeightedDeletion.scalar_cut_of_leading line 1780
  269. theorem OAI.DeligneDrinfeld.WeightedDeletion.scalar_zero_of_cost line 1803
  270. def OAI.DeligneDrinfeld.EmbeddedTerminal.κ line 1821
  271. theorem OAI.DeligneDrinfeld.EmbeddedTerminal.raw_snoc line 1824
  272. theorem OAI.DeligneDrinfeld.EmbeddedTerminal.scalar_word line 1843
  273. theorem OAI.DeligneDrinfeld.EmbeddedTerminal.test line 1885
  274. def OAI.DeligneDrinfeld.WordReversal.rev line 1904
  275. theorem OAI.DeligneDrinfeld.WordReversal.rev_word line 1908
  276. theorem OAI.DeligneDrinfeld.WordReversal.rev_atom line 1911
  277. theorem OAI.DeligneDrinfeld.WordReversal.rev_one line 1914
  278. theorem OAI.DeligneDrinfeld.WordReversal.rev_mul line 1916
  279. theorem OAI.DeligneDrinfeld.WordReversal.rev_coeff line 1929
  280. theorem OAI.DeligneDrinfeld.WordReversal.rev_lie_charTwo line 1947
  281. theorem OAI.DeligneDrinfeld.WordReversal.coeff_reverse_charTwo line 1964
  282. inductive OAI.DeligneDrinfeld.RowKernel.Row line 1974
  283. instance OAI.DeligneDrinfeld.RowKernel.(instance at line 1975) line 1975
  284. def OAI.DeligneDrinfeld.RowKernel.κ line 1977
  285. def OAI.DeligneDrinfeld.RowKernel.enc line 1993
  286. theorem OAI.DeligneDrinfeld.RowKernel.enc_injective line 1995
  287. theorem OAI.DeligneDrinfeld.RowKernel.enc_not_w line 1997
  288. theorem OAI.DeligneDrinfeld.RowKernel.enc_eq_e line 1999
  289. theorem OAI.DeligneDrinfeld.RowKernel.enc_eq_p line 2000
  290. def OAI.DeligneDrinfeld.RowKernel.aCount line 2002
  291. def OAI.DeligneDrinfeld.RowKernel.cCount line 2003
  292. def OAI.DeligneDrinfeld.RowKernel.eCount line 2004
  293. def OAI.DeligneDrinfeld.RowKernel.pCount line 2005
  294. theorem OAI.DeligneDrinfeld.RowKernel.count_enc_e line 2007
  295. theorem OAI.DeligneDrinfeld.RowKernel.count_enc_p line 2012
  296. theorem OAI.DeligneDrinfeld.RowKernel.a_cost line 2017
  297. theorem OAI.DeligneDrinfeld.RowKernel.one_cost line 2020
  298. theorem OAI.DeligneDrinfeld.RowKernel.three_cost line 2022
  299. theorem OAI.DeligneDrinfeld.RowKernel.cut_two line 2024
  300. theorem OAI.DeligneDrinfeld.RowKernel.cut_four line 2029
  301. def OAI.DeligneDrinfeld.RowKernel.good line 2034
  302. theorem OAI.DeligneDrinfeld.RowKernel.good_enc line 2036
  303. theorem OAI.DeligneDrinfeld.RowKernel.enc_no_w line 2039
  304. def OAI.DeligneDrinfeld.RowKernel.test line 2044
  305. theorem OAI.DeligneDrinfeld.RowKernel.test_cut line 2047
  306. theorem OAI.DeligneDrinfeld.RowKernel.degree_zero line 2053
  307. theorem OAI.DeligneDrinfeld.RowKernel.test_one line 2056
  308. theorem OAI.DeligneDrinfeld.RowKernel.test_two line 2067
  309. theorem OAI.DeligneDrinfeld.RowKernel.test_three line 2072
  310. theorem OAI.DeligneDrinfeld.RowKernel.test_four line 2077
  311. def OAI.DeligneDrinfeld.RowKernel.Equation line 2083
  312. theorem OAI.DeligneDrinfeld.RowKernel.coefficient_bad line 2086
  313. theorem OAI.DeligneDrinfeld.RowKernel.degree_reverse line 2096
  314. theorem OAI.DeligneDrinfeld.RowKernel.aCount_eq_count line 2100
  315. theorem OAI.DeligneDrinfeld.RowKernel.cCount_eq_count line 2108
  316. theorem OAI.DeligneDrinfeld.RowKernel.all_A_of_good_both line 2116
  317. theorem OAI.DeligneDrinfeld.RowKernel.not_good_reverse line 2132
  318. theorem OAI.DeligneDrinfeld.RowKernel.coefficient_minimal line 2141
  319. def OAI.DeligneDrinfeld.RowKernel.acCount line 2157
  320. def OAI.DeligneDrinfeld.RowKernel.bCount line 2159
  321. theorem OAI.DeligneDrinfeld.RowKernel.degree_ac line 2161
  322. theorem OAI.DeligneDrinfeld.RowKernel.kernel_support line 2166
  323. def OAI.DeligneDrinfeld.LetterRetraction.assoc line 2212
  324. def OAI.DeligneDrinfeld.LetterRetraction.lie line 2213
  325. theorem OAI.DeligneDrinfeld.LetterRetraction.assoc_atom line 2216
  326. theorem OAI.DeligneDrinfeld.LetterRetraction.lie_of line 2219
  327. theorem OAI.DeligneDrinfeld.LetterRetraction.embed_lie line 2222
  328. theorem OAI.DeligneDrinfeld.LetterRetraction.assoc_word line 2230
  329. theorem OAI.DeligneDrinfeld.LetterRetraction.coeff line 2241
  330. theorem OAI.DeligneDrinfeld.LetterRetraction.assoc_eq_self line 2253
  331. theorem OAI.DeligneDrinfeld.LetterRetraction.lie_eq_self line 2262
  332. def OAI.DeligneDrinfeld.LetterRetraction.sub line 2267
  333. theorem OAI.DeligneDrinfeld.LetterRetraction.lie_mem line 2270
  334. theorem OAI.DeligneDrinfeld.LetterRetraction.mem_of_support line 2282
  335. theorem OAI.DeligneDrinfeld.RowKernel.degree_indicator_zero line 2291
  336. theorem OAI.DeligneDrinfeld.RowKernel.no_A_coeff line 2300
  337. theorem OAI.DeligneDrinfeld.RowKernel.kernel_no_C line 2310
  338. theorem OAI.DeligneDrinfeld.WeightedDeletion.edge_raw line 2328
  339. theorem OAI.DeligneDrinfeld.WeightedDeletion.edge_op line 2334
  340. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_support line 2341
  341. theorem OAI.DeligneDrinfeld.WeightedDeletion.action_word_support line 2354
  342. theorem OAI.DeligneDrinfeld.WeightedDeletion.raw_congr_on line 2363
  343. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_congr_on line 2372
  344. theorem OAI.DeligneDrinfeld.WeightedDeletion.action_congr_on line 2384
  345. theorem OAI.DeligneDrinfeld.WeightedDeletion.scalar_cut_of_homogeneous line 2400
  346. theorem OAI.DeligneDrinfeld.WeightedDeletion.scalar_zero_of_low line 2413
  347. abbrev OAI.DeligneDrinfeld.LeadingRows.E line 2431
  348. def OAI.DeligneDrinfeld.LeadingRows.toLetter line 2433
  349. def OAI.DeligneDrinfeld.LeadingRows.edge line 2435
  350. def OAI.DeligneDrinfeld.LeadingRows.slots line 2437
  351. def OAI.DeligneDrinfeld.LeadingRows.subst line 2451
  352. def OAI.DeligneDrinfeld.LeadingRows.slotEdge line 2454
  353. def OAI.DeligneDrinfeld.LeadingRows.κ₀ line 2457
  354. def OAI.DeligneDrinfeld.LeadingRows.zeroCount line 2459
  355. theorem OAI.DeligneDrinfeld.LeadingRows.zero_cost line 2461
  356. theorem OAI.DeligneDrinfeld.LeadingRows.cut_table line 2464
  357. def OAI.DeligneDrinfeld.LeadingRows.operators line 2468
  358. theorem OAI.DeligneDrinfeld.LeadingRows.substituted_action line 2471
  359. theorem OAI.DeligneDrinfeld.LeadingRows.count_enc_zero line 2481
  360. theorem OAI.DeligneDrinfeld.LeadingRows.scalar_allocated line 2488
  361. def OAI.DeligneDrinfeld.LeadingRows.namedCount line 2506
  362. def OAI.DeligneDrinfeld.LeadingRows.namedκ line 2507
  363. theorem OAI.DeligneDrinfeld.LeadingRows.named_zero_cost line 2509
  364. theorem OAI.DeligneDrinfeld.LeadingRows.named_action line 2512
  365. def OAI.DeligneDrinfeld.LeadingRows.P line 2518
  366. theorem OAI.DeligneDrinfeld.LeadingRows.scalar_subst line 2520
  367. theorem OAI.DeligneDrinfeld.LeadingRows.equation_of_low_interpretation line 2530
  368. def OAI.DeligneDrinfeld.LeadingRows.secondExtra line 2550
  369. def OAI.DeligneDrinfeld.LeadingRows.secondPairs line 2554
  370. def OAI.DeligneDrinfeld.LeadingRows.secondEdge line 2556
  371. theorem OAI.DeligneDrinfeld.LeadingRows.second_curvature line 2558
  372. theorem OAI.DeligneDrinfeld.LeadingRows.second_common line 2562
  373. def OAI.DeligneDrinfeld.LeadingRows.secondFiber line 2567
  374. def OAI.DeligneDrinfeld.LeadingRows.secondBase line 2569
  375. theorem OAI.DeligneDrinfeld.LeadingRows.second_sum line 2572
  376. theorem OAI.DeligneDrinfeld.LeadingRows.second_action line 2581
  377. theorem OAI.DeligneDrinfeld.LeadingRows.second_evaluate line 2594
  378. theorem OAI.DeligneDrinfeld.LeadingRows.second_order_correct line 2602
  379. theorem OAI.DeligneDrinfeld.LeadingRows.main_action line 2611
  380. theorem OAI.DeligneDrinfeld.LeadingRows.main_evaluate line 2619
  381. theorem OAI.DeligneDrinfeld.LeadingRows.target_order_correct line 2625
  382. theorem OAI.DeligneDrinfeld.LeadingRows.equation_from_source_order line 2631
  383. theorem OAI.DeligneDrinfeld.WordGrading.algHom_difference_above line 2647
  384. abbrev OAI.DeligneDrinfeld.ExactPentagon.u12 line 2676
  385. abbrev OAI.DeligneDrinfeld.ExactPentagon.u23 line 2677
  386. def OAI.DeligneDrinfeld.ExactPentagon.extra line 2679
  387. def OAI.DeligneDrinfeld.ExactPentagon.exactTwo line 2684
  388. def OAI.DeligneDrinfeld.ExactPentagon.omitted line 2687
  389. def OAI.DeligneDrinfeld.ExactPentagon.weight line 2690
  390. def OAI.DeligneDrinfeld.ExactPentagon.full line 2692
  391. theorem OAI.DeligneDrinfeld.ExactPentagon.atom_homo line 2695
  392. theorem OAI.DeligneDrinfeld.ExactPentagon.subst_homo line 2698
  393. theorem OAI.DeligneDrinfeld.ExactPentagon.P_homogeneous line 2709
  394. theorem OAI.DeligneDrinfeld.ExactPentagon.u12_homo line 2715
  395. theorem OAI.DeligneDrinfeld.ExactPentagon.u23_homo line 2716
  396. theorem OAI.DeligneDrinfeld.ExactPentagon.extra_homo line 2718
  397. theorem OAI.DeligneDrinfeld.ExactPentagon.exactTwo_difference line 2729
  398. theorem OAI.DeligneDrinfeld.ExactPentagon.exactTwo_above line 2736
  399. theorem OAI.DeligneDrinfeld.ExactPentagon.omitted_weight line 2743
  400. theorem OAI.DeligneDrinfeld.ExactPentagon.full_error line 2755
  401. theorem OAI.DeligneDrinfeld.ExactPentagon.row_equation line 2775
  402. theorem OAI.DeligneDrinfeld.AssociativeEvaluation.lift_embed line 2792
  403. theorem OAI.DeligneDrinfeld.AssociativeEvaluation.map_eval line 2801
  404. theorem OAI.DeligneDrinfeld.CharTwoAction.square_add line 2814
  405. abbrev OAI.DeligneDrinfeld.ExactPentagon.K line 2821
  406. abbrev OAI.DeligneDrinfeld.ExactPentagon.U13 line 2824
  407. abbrev OAI.DeligneDrinfeld.ExactPentagon.U23 line 2825
  408. abbrev OAI.DeligneDrinfeld.ExactPentagon.X1 line 2826
  409. abbrev OAI.DeligneDrinfeld.ExactPentagon.X2 line 2827
  410. abbrev OAI.DeligneDrinfeld.ExactPentagon.U12 line 2828
  411. def OAI.DeligneDrinfeld.ExactPentagon.algEval line 2830
  412. def OAI.DeligneDrinfeld.ExactPentagon.quad line 2833
  413. def OAI.DeligneDrinfeld.ExactPentagon.quadEval line 2838
  414. theorem OAI.DeligneDrinfeld.ExactPentagon.algEval_quad line 2841
  415. def OAI.DeligneDrinfeld.ExactPentagon.interpretation line 2847
  416. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_base line 2849
  417. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_fiber line 2851
  418. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_a1 line 2854
  419. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_a2 line 2857
  420. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_u12 line 2860
  421. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_u13 line 2863
  422. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_u23 line 2865
  423. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_v12 line 2867
  424. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_v13 line 2870
  425. theorem OAI.DeligneDrinfeld.ExactPentagon.interpretation_v23 line 2873
  426. theorem OAI.DeligneDrinfeld.ExactPentagon.cross13 line 2877
  427. theorem OAI.DeligneDrinfeld.ExactPentagon.cross23 line 2880
  428. theorem OAI.DeligneDrinfeld.ExactPentagon.base_triple line 2884
  429. theorem OAI.DeligneDrinfeld.ExactPentagon.base_triangle line 2894
  430. theorem OAI.DeligneDrinfeld.ExactPentagon.interprets_one line 2906
  431. theorem OAI.DeligneDrinfeld.ExactPentagon.interprets_four line 2914
  432. theorem OAI.DeligneDrinfeld.ExactPentagon.interprets_omitted line 2920
  433. theorem OAI.DeligneDrinfeld.ExactPentagon.interprets_two line 2926
  434. theorem OAI.DeligneDrinfeld.ExactPentagon.interprets_three line 2944
  435. theorem OAI.DeligneDrinfeld.ExactPentagon.full_interpretation line 2962
  436. def OAI.DeligneDrinfeld.ExactPentagon.labels line 2972
  437. def OAI.DeligneDrinfeld.ExactPentagon.sourceHom line 2985
  438. theorem OAI.DeligneDrinfeld.ExactPentagon.sourceHom_t line 2988
  439. theorem OAI.DeligneDrinfeld.ExactPentagon.sourceHom_01 line 2991
  440. theorem OAI.DeligneDrinfeld.ExactPentagon.sourceHom_02 line 2994
  441. theorem OAI.DeligneDrinfeld.ExactPentagon.sourceHom_12 line 2997
  442. theorem OAI.DeligneDrinfeld.ExactPentagon.sourceHom_13 line 3000
  443. theorem OAI.DeligneDrinfeld.ExactPentagon.sourceHom_23 line 3005
  444. theorem OAI.DeligneDrinfeld.ExactPentagon.eval_quadratic line 3011
  445. theorem OAI.DeligneDrinfeld.ExactPentagon.full_zero line 3018