OAI/Algebra/Drinfeld/Foundations.lean

GitHub source file

937 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.freeLie_induction line 8
  2. abbrev OAI.DeligneDrinfeld.L line 30

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:8 (same declaration text).

  3. def OAI.DeligneDrinfeld.x line 31

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:9 (same declaration text).

  4. def OAI.DeligneDrinfeld.y line 32

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:10 (same declaration text).

  5. def OAI.DeligneDrinfeld.eval line 34

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:12 (same declaration text).

  6. abbrev OAI.DeligneDrinfeld.Edge line 37

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:15 (same declaration text).

  7. abbrev OAI.DeligneDrinfeld.BraidFree line 38

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:16 (same declaration text).

  8. def OAI.DeligneDrinfeld.chord line 40

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:18 (same declaration text).

  9. def OAI.DeligneDrinfeld.braidRelations line 44

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:22 (same declaration text).

  10. def OAI.DeligneDrinfeld.braidIdeal line 51

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:29 (same declaration text).

  11. abbrev OAI.DeligneDrinfeld.T4 line 54

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:32 (same declaration text).

  12. def OAI.DeligneDrinfeld.t line 55

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:33 (same declaration text).

  13. def OAI.DeligneDrinfeld.IsSolution line 57

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:35 (same declaration text).

  14. def OAI.DeligneDrinfeld.W line 64

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:42 (same declaration text).

  15. structure OAI.DeligneDrinfeld.Tangent line 97

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:75 (same declaration text).

  16. def OAI.DeligneDrinfeld.Tangent.equiv line 101

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:79 (same declaration text).

  17. instance OAI.DeligneDrinfeld.(instance at line 107) line 107
  18. instance OAI.DeligneDrinfeld.(instance at line 108) line 108
  19. instance OAI.DeligneDrinfeld.(instance at line 109) line 109
  20. theorem OAI.DeligneDrinfeld.Tangent.ext line 113
  21. theorem OAI.DeligneDrinfeld.Tangent.base_zero line 116
  22. theorem OAI.DeligneDrinfeld.Tangent.velocity_zero line 117
  23. theorem OAI.DeligneDrinfeld.Tangent.base_add line 118
  24. theorem OAI.DeligneDrinfeld.Tangent.velocity_add line 119
  25. theorem OAI.DeligneDrinfeld.Tangent.base_smul line 121
  26. theorem OAI.DeligneDrinfeld.Tangent.velocity_smul line 122
  27. theorem OAI.DeligneDrinfeld.Tangent.base_lie line 124
  28. theorem OAI.DeligneDrinfeld.Tangent.velocity_lie line 125
  29. instance OAI.DeligneDrinfeld.(instance at line 128) line 128
  30. instance OAI.DeligneDrinfeld.(instance at line 167) line 167
  31. def OAI.DeligneDrinfeld.tangentLift line 176

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:139 (same declaration text).

  32. def OAI.DeligneDrinfeld.D line 179

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:142 (same declaration text).

  33. def OAI.DeligneDrinfeld.ihara line 181

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:144 (same declaration text).

  34. theorem OAI.DeligneDrinfeld.eval_x line 183
  35. theorem OAI.DeligneDrinfeld.eval_y line 185
  36. def OAI.DeligneDrinfeld.Tangent.baseHom line 188
  37. theorem OAI.DeligneDrinfeld.tangentLift_base line 194
  38. theorem OAI.DeligneDrinfeld.D_x line 201
  39. theorem OAI.DeligneDrinfeld.D_y line 202
  40. theorem OAI.DeligneDrinfeld.D_zero line 203
  41. theorem OAI.DeligneDrinfeld.D_add line 204
  42. theorem OAI.DeligneDrinfeld.D_smul line 205
  43. theorem OAI.DeligneDrinfeld.D_lie line 206
  44. def OAI.DeligneDrinfeld.derivation line 209
  45. theorem OAI.DeligneDrinfeld.derivation_apply line 217
  46. theorem OAI.DeligneDrinfeld.derivation_ext line 219
  47. theorem OAI.DeligneDrinfeld.D_zero_left line 229
  48. theorem OAI.DeligneDrinfeld.D_add_left line 234
  49. theorem OAI.DeligneDrinfeld.D_smul_left line 239
  50. inductive OAI.DeligneDrinfeld.WeightedWord line 244

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:146 (same declaration text).

  51. def OAI.DeligneDrinfeld.weightPiece line 249

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:151 (same declaration text).

  52. abbrev OAI.DeligneDrinfeld.OddFree line 252

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:154 (same declaration text).

  53. def OAI.DeligneDrinfeld.oddWeight line 253

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:155 (same declaration text).

  54. abbrev OAI.DeligneDrinfeld.Fn line 254

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:156 (same declaration text).

  55. abbrev OAI.DeligneDrinfeld.Ln line 255

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:157 (same declaration text).

  56. abbrev OAI.DeligneDrinfeld.Wn line 256

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:158 (same declaration text).

  57. def OAI.DeligneDrinfeld.Graded line 258

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:160 (same declaration text).

  58. abbrev OAI.DeligneDrinfeld.OddCompletion line 261

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:163 (same declaration text).

  59. abbrev OAI.DeligneDrinfeld.WCompletion line 262

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:164 (same declaration text).

  60. instance OAI.DeligneDrinfeld.(instance at line 264) line 264
  61. instance OAI.DeligneDrinfeld.(instance at line 265) line 265
  62. def OAI.DeligneDrinfeld.completed line 267

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:169 (same declaration text).

  63. def OAI.DeligneDrinfeld.completedInv line 270

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:172 (same declaration text).

  64. def OAI.DeligneDrinfeld.MainStatement line 276

    Also declared: ComparatorChallenges/DeligneDrinfeld.lean:178 (same declaration text).

  65. abbrev OAI.DeligneDrinfeld.AssociativeModel.FL line 290
  66. abbrev OAI.DeligneDrinfeld.AssociativeModel.A line 291
  67. def OAI.DeligneDrinfeld.AssociativeModel.atom line 294
  68. def OAI.DeligneDrinfeld.AssociativeModel.embed line 296
  69. theorem OAI.DeligneDrinfeld.AssociativeModel.embed_of line 298
  70. def OAI.DeligneDrinfeld.AssociativeModel.dynkinWord line 301
  71. theorem OAI.DeligneDrinfeld.AssociativeModel.dynkinWord_cons line 306
  72. def OAI.DeligneDrinfeld.AssociativeModel.wordLinear line 312
  73. theorem OAI.DeligneDrinfeld.AssociativeModel.wordLinear_single line 316
  74. def OAI.DeligneDrinfeld.AssociativeModel.dynkin line 321
  75. def OAI.DeligneDrinfeld.AssociativeModel.wordAct line 323
  76. def OAI.DeligneDrinfeld.AssociativeModel.act line 326
  77. theorem OAI.DeligneDrinfeld.AssociativeModel.act_single line 329
  78. theorem OAI.DeligneDrinfeld.AssociativeModel.wordAct_of_apply line 332
  79. theorem OAI.DeligneDrinfeld.AssociativeModel.act_embed line 336
  80. theorem OAI.DeligneDrinfeld.AssociativeModel.dynkinWord_append line 343
  81. def OAI.DeligneDrinfeld.AssociativeModel.homogeneous line 351
  82. theorem OAI.DeligneDrinfeld.AssociativeModel.single_mem_homogeneous line 355
  83. theorem OAI.DeligneDrinfeld.AssociativeModel.mul_homogeneous line 359
  84. theorem OAI.DeligneDrinfeld.AssociativeModel.dynkin_mul line 376
  85. theorem OAI.DeligneDrinfeld.AssociativeModel.dynkin_embed_word line 391
  86. def OAI.DeligneDrinfeld.AssociativeModel.normalizedDynkin line 415
  87. theorem OAI.DeligneDrinfeld.AssociativeModel.normalizedDynkin_homogeneous line 418
  88. theorem OAI.DeligneDrinfeld.AssociativeModel.normalizedDynkin_embed_word line 429
  89. theorem OAI.DeligneDrinfeld.AssociativeModel.mem_word_span line 435
  90. theorem OAI.DeligneDrinfeld.AssociativeModel.normalizedDynkin_embed line 459
  91. theorem OAI.DeligneDrinfeld.AssociativeModel.embed_injective line 469
  92. structure OAI.DeligneDrinfeld.FreeDerivations.Jet line 479
  93. def OAI.DeligneDrinfeld.FreeDerivations.Jet.equiv line 483
  94. instance OAI.DeligneDrinfeld.FreeDerivations.(instance at line 489) line 489
  95. instance OAI.DeligneDrinfeld.FreeDerivations.(instance at line 490) line 490
  96. instance OAI.DeligneDrinfeld.FreeDerivations.(instance at line 491) line 491
  97. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.ext line 495
  98. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.base_zero line 498
  99. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.velocity_zero line 499
  100. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.base_add line 500
  101. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.velocity_add line 501
  102. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.base_smul line 503
  103. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.velocity_smul line 504
  104. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.base_lie line 506
  105. theorem OAI.DeligneDrinfeld.FreeDerivations.Jet.velocity_lie line 507
  106. instance OAI.DeligneDrinfeld.FreeDerivations.(instance at line 510) line 510
  107. instance OAI.DeligneDrinfeld.FreeDerivations.(instance at line 520) line 520
  108. def OAI.DeligneDrinfeld.FreeDerivations.Jet.baseHom line 523
  109. def OAI.DeligneDrinfeld.FreeDerivations.jetLift line 532
  110. theorem OAI.DeligneDrinfeld.FreeDerivations.jetLift_base line 535
  111. def OAI.DeligneDrinfeld.FreeDerivations.extend line 544
  112. theorem OAI.DeligneDrinfeld.FreeDerivations.extend_of line 559
  113. theorem OAI.DeligneDrinfeld.FreeDerivations.ext line 564
  114. theorem OAI.DeligneDrinfeld.FreeDerivations.extend_unique line 574
  115. def OAI.DeligneDrinfeld.FreeDerivations.pair line 581
  116. theorem OAI.DeligneDrinfeld.FreeDerivations.pair_of_left line 585
  117. theorem OAI.DeligneDrinfeld.FreeDerivations.pair_of_right line 589
  118. theorem OAI.DeligneDrinfeld.FreeDerivations.pair_of_other line 595
  119. theorem OAI.DeligneDrinfeld.FreeDerivations.pair_comm line 599
  120. theorem OAI.DeligneDrinfeld.FreeDerivations.pair_self line 608
  121. theorem OAI.DeligneDrinfeld.FreeDerivations.pair_disjoint line 615
  122. theorem OAI.DeligneDrinfeld.FreeDerivations.pair_three line 630
  123. def OAI.DeligneDrinfeld.BraidRepresentation.fiber line 657
  124. def OAI.DeligneDrinfeld.BraidRepresentation.base line 658
  125. def OAI.DeligneDrinfeld.BraidRepresentation.chord line 660
  126. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_none_none line 666
  127. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_none_some line 667
  128. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_some_none line 668
  129. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_some_some line 669
  130. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_comm line 671
  131. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_self line 674
  132. theorem OAI.DeligneDrinfeld.BraidRepresentation.base_fiber line 677
  133. theorem OAI.DeligneDrinfeld.BraidRepresentation.fiber_base line 682
  134. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_disjoint line 687
  135. theorem OAI.DeligneDrinfeld.BraidRepresentation.chord_three line 694
  136. abbrev OAI.DeligneDrinfeld.BraidModel.Fiber line 733
  137. abbrev OAI.DeligneDrinfeld.BraidModel.Der line 734
  138. abbrev OAI.DeligneDrinfeld.BraidModel.Model line 735
  139. def OAI.DeligneDrinfeld.BraidModel.chord line 736
  140. theorem OAI.DeligneDrinfeld.BraidModel.chord_comm line 739
  141. theorem OAI.DeligneDrinfeld.BraidModel.chord_self line 742
  142. def OAI.DeligneDrinfeld.BraidModel.preMap line 745
  143. theorem OAI.DeligneDrinfeld.BraidModel.preMap_chord line 747
  144. theorem OAI.DeligneDrinfeld.BraidModel.ideal_le_ker line 756
  145. def OAI.DeligneDrinfeld.BraidModel.map line 770
  146. theorem OAI.DeligneDrinfeld.BraidModel.map_t line 778
  147. theorem OAI.DeligneDrinfeld.AssociativeModel.coeff_rotate line 786
  148. theorem OAI.DeligneDrinfeld.AssociativeModel.coeff_starts_ne line 797
  149. theorem OAI.DeligneDrinfeld.AssociativeModel.coeff_contains_ne line 807
  150. theorem OAI.DeligneDrinfeld.AssociativeModel.coeff_eq_zero_of_letter_ne line 818
  151. theorem OAI.DeligneDrinfeld.AssociativeModel.dynkinWord_all_eq line 824
  152. theorem OAI.DeligneDrinfeld.AssociativeModel.centralizer_generator line 840
  153. theorem OAI.DeligneDrinfeld.map_eval line 864
  154. theorem OAI.DeligneDrinfeld.eval_self line 873
  155. theorem OAI.DeligneDrinfeld.eval_commutes line 878
  156. theorem OAI.DeligneDrinfeld.chord_comm line 888
  157. theorem OAI.DeligneDrinfeld.t_comm line 892
  158. theorem OAI.DeligneDrinfeld.t_disjoint line 896
  159. theorem OAI.DeligneDrinfeld.t_three line 903
  160. def OAI.DeligneDrinfeld.BraidModel.inclusion line 911
  161. theorem OAI.DeligneDrinfeld.BraidModel.map_inclusion line 914
  162. theorem OAI.DeligneDrinfeld.BraidModel.inclusion_injective line 919
  163. theorem OAI.DeligneDrinfeld.commute_symm line 929
  164. theorem OAI.DeligneDrinfeld.evals_commute line 932
  165. theorem OAI.DeligneDrinfeld.eval_add_of_commuting line 940
  166. theorem OAI.DeligneDrinfeld.eval_vanish_of_commuting line 955
  167. theorem OAI.DeligneDrinfeld.eval_central_shift line 969
  168. def OAI.DeligneDrinfeld.T4Universal.pre line 979
  169. theorem OAI.DeligneDrinfeld.T4Universal.pre_chord line 982
  170. def OAI.DeligneDrinfeld.T4Universal.lift line 993
  171. theorem OAI.DeligneDrinfeld.T4Universal.lift_t line 1012
  172. theorem OAI.DeligneDrinfeld.t_self line 1017
  173. def OAI.DeligneDrinfeld.t4Rename line 1019
  174. theorem OAI.DeligneDrinfeld.t4Rename_t line 1028
  175. theorem OAI.DeligneDrinfeld.solution_swap line 1031
  176. theorem OAI.DeligneDrinfeld.solution_three line 1038
  177. theorem OAI.DeligneDrinfeld.free_action_inner line 1044
  178. def OAI.DeligneDrinfeld.InnerSemiDirect.lift line 1081
  179. theorem OAI.DeligneDrinfeld.InnerSemiDirect.lift_inl line 1091
  180. theorem OAI.DeligneDrinfeld.InnerSemiDirect.lift_inr line 1093
  181. abbrev OAI.DeligneDrinfeld.SpecialFiber.F line 1099
  182. def OAI.DeligneDrinfeld.SpecialFiber.fa line 1100
  183. def OAI.DeligneDrinfeld.SpecialFiber.fb line 1101
  184. def OAI.DeligneDrinfeld.SpecialFiber.fc line 1102
  185. def OAI.DeligneDrinfeld.SpecialFiber.action line 1104
  186. abbrev OAI.DeligneDrinfeld.SpecialFiber.M line 1105
  187. def OAI.DeligneDrinfeld.SpecialFiber.a line 1107
  188. def OAI.DeligneDrinfeld.SpecialFiber.b line 1108
  189. def OAI.DeligneDrinfeld.SpecialFiber.c line 1109
  190. def OAI.DeligneDrinfeld.SpecialFiber.u line 1110
  191. def OAI.DeligneDrinfeld.SpecialFiber.v line 1111
  192. def OAI.DeligneDrinfeld.SpecialFiber.w line 1112
  193. theorem OAI.DeligneDrinfeld.SpecialFiber.au line 1114
  194. theorem OAI.DeligneDrinfeld.SpecialFiber.bu line 1117
  195. theorem OAI.DeligneDrinfeld.SpecialFiber.cu line 1120
  196. theorem OAI.DeligneDrinfeld.SpecialFiber.av line 1123
  197. theorem OAI.DeligneDrinfeld.SpecialFiber.bv line 1126
  198. theorem OAI.DeligneDrinfeld.SpecialFiber.cv line 1129
  199. def OAI.DeligneDrinfeld.SpecialFiber.chord line 1133
  200. theorem OAI.DeligneDrinfeld.SpecialFiber.chord_symm line 1143
  201. theorem OAI.DeligneDrinfeld.SpecialFiber.chord_zero line 1146
  202. theorem OAI.DeligneDrinfeld.SpecialFiber.chord_disjoint line 1148
  203. theorem OAI.DeligneDrinfeld.SpecialFiber.chord_three line 1159
  204. def OAI.DeligneDrinfeld.SpecialFiber.representation line 1169
  205. theorem OAI.DeligneDrinfeld.SpecialFiber.representation_t line 1172
  206. def OAI.DeligneDrinfeld.SpecialFiber.fiberSpec line 1175
  207. def OAI.DeligneDrinfeld.SpecialFiber.baseSpec line 1177
  208. theorem OAI.DeligneDrinfeld.SpecialFiber.fiberSpec_fa line 1179
  209. theorem OAI.DeligneDrinfeld.SpecialFiber.fiberSpec_fb line 1180
  210. theorem OAI.DeligneDrinfeld.SpecialFiber.fiberSpec_fc line 1181
  211. theorem OAI.DeligneDrinfeld.SpecialFiber.baseSpec_x line 1182
  212. theorem OAI.DeligneDrinfeld.SpecialFiber.baseSpec_y line 1183
  213. theorem OAI.DeligneDrinfeld.SpecialFiber.spec_equivariant line 1185
  214. def OAI.DeligneDrinfeld.SpecialFiber.specialize line 1193
  215. theorem OAI.DeligneDrinfeld.SpecialFiber.specialize_a line 1195
  216. theorem OAI.DeligneDrinfeld.SpecialFiber.specialize_b line 1196
  217. theorem OAI.DeligneDrinfeld.SpecialFiber.specialize_c line 1197
  218. theorem OAI.DeligneDrinfeld.SpecialFiber.specialize_u line 1198
  219. theorem OAI.DeligneDrinfeld.SpecialFiber.specialize_v line 1199
  220. theorem OAI.DeligneDrinfeld.SpecialFiber.eval_right line 1201
  221. def OAI.DeligneDrinfeld.SpecialFiber.Fa line 1205
  222. def OAI.DeligneDrinfeld.SpecialFiber.Fb line 1206
  223. def OAI.DeligneDrinfeld.SpecialFiber.Fc line 1207
  224. theorem OAI.DeligneDrinfeld.SpecialFiber.Fa_inl line 1209
  225. theorem OAI.DeligneDrinfeld.SpecialFiber.Fb_inl line 1213
  226. theorem OAI.DeligneDrinfeld.SpecialFiber.Fc_inl line 1217
  227. theorem OAI.DeligneDrinfeld.SpecialFiber.eval_comm_a line 1222
  228. theorem OAI.DeligneDrinfeld.SpecialFiber.eval_comm_b line 1226
  229. theorem OAI.DeligneDrinfeld.SpecialFiber.eval_comm_c line 1230
  230. theorem OAI.DeligneDrinfeld.SpecialFiber.eval_comm_sum line 1234
  231. theorem OAI.DeligneDrinfeld.SpecialFiber.fiber_identity line 1239
  232. theorem OAI.DeligneDrinfeld.SpecialFiber.Fb_specialize line 1250
  233. theorem OAI.DeligneDrinfeld.SpecialFiber.pentagon line 1261
  234. theorem OAI.DeligneDrinfeld.SpecialFiber.pentagon_reverse line 1267
  235. theorem OAI.DeligneDrinfeld.SpecialFiber.eval_bv_shift line 1274
  236. theorem OAI.DeligneDrinfeld.SpecialFiber.eval_bu_shift line 1284
  237. theorem OAI.DeligneDrinfeld.SpecialFiber.delta_a line 1294
  238. theorem OAI.DeligneDrinfeld.SpecialFiber.delta_c line 1304
  239. theorem OAI.DeligneDrinfeld.Differentiation.Jet.base_neg line 1322
  240. theorem OAI.DeligneDrinfeld.Differentiation.Jet.velocity_neg line 1323
  241. theorem OAI.DeligneDrinfeld.Differentiation.Jet.base_sub line 1324
  242. theorem OAI.DeligneDrinfeld.Differentiation.Jet.velocity_sub line 1325
  243. theorem OAI.DeligneDrinfeld.Differentiation.Jet.mk_add line 1327
  244. theorem OAI.DeligneDrinfeld.Differentiation.Jet.mk_neg line 1329
  245. theorem OAI.DeligneDrinfeld.Differentiation.Jet.mk_sub line 1331
  246. theorem OAI.DeligneDrinfeld.Differentiation.eval_base line 1334
  247. def OAI.DeligneDrinfeld.Differentiation.adPower line 1337
  248. theorem OAI.DeligneDrinfeld.Differentiation.adPower_zero line 1342
  249. theorem OAI.DeligneDrinfeld.Differentiation.adPower_succ line 1344
  250. theorem OAI.DeligneDrinfeld.Differentiation.adPower_smul line 1345
  251. theorem OAI.DeligneDrinfeld.Differentiation.adPower_zero_right line 1349
  252. theorem OAI.DeligneDrinfeld.Differentiation.adPower_self line 1352
  253. theorem OAI.DeligneDrinfeld.Differentiation.adPower_zero_left line 1360
  254. def OAI.DeligneDrinfeld.Differentiation.slope line 1363
  255. theorem OAI.DeligneDrinfeld.Differentiation.slope_x line 1366
  256. theorem OAI.DeligneDrinfeld.Differentiation.slope_y line 1367
  257. theorem OAI.DeligneDrinfeld.Differentiation.slope_zero line 1368
  258. theorem OAI.DeligneDrinfeld.Differentiation.slope_add line 1369
  259. theorem OAI.DeligneDrinfeld.Differentiation.slope_smul line 1371
  260. theorem OAI.DeligneDrinfeld.Differentiation.slope_lie line 1373
  261. theorem OAI.DeligneDrinfeld.Differentiation.slope_zero_direction line 1377
  262. theorem OAI.DeligneDrinfeld.Differentiation.slope_add_direction line 1385
  263. theorem OAI.DeligneDrinfeld.Differentiation.slope_smul_direction line 1394
  264. theorem OAI.DeligneDrinfeld.Differentiation.word_pos line 1403
  265. def OAI.DeligneDrinfeld.Differentiation.DiagonalData line 1408
  266. theorem OAI.DeligneDrinfeld.Differentiation.diagonal_bracket line 1413
  267. theorem OAI.DeligneDrinfeld.Differentiation.diagonal_word line 1461
  268. theorem OAI.DeligneDrinfeld.Differentiation.diagonal_homogeneous line 1480
  269. theorem OAI.DeligneDrinfeld.Differentiation.slope_neg_direction line 1502
  270. theorem OAI.DeligneDrinfeld.Differentiation.slope_inner line 1506
  271. theorem OAI.DeligneDrinfeld.Differentiation.slope_swap line 1515
  272. theorem OAI.DeligneDrinfeld.Differentiation.diagonal_slope line 1519
  273. theorem OAI.DeligneDrinfeld.Differentiation.diagonal_first line 1524
  274. def OAI.DeligneDrinfeld.Differentiation.G line 1535
  275. theorem OAI.DeligneDrinfeld.Differentiation.eval_G line 1537
  276. theorem OAI.DeligneDrinfeld.Differentiation.slope_G line 1541
  277. def OAI.DeligneDrinfeld.Differentiation.fiberEval line 1557
  278. theorem OAI.DeligneDrinfeld.Differentiation.fiberEval_fa line 1559
  279. theorem OAI.DeligneDrinfeld.Differentiation.fiberEval_fb line 1561
  280. theorem OAI.DeligneDrinfeld.Differentiation.fiberEval_fc line 1563
  281. theorem OAI.DeligneDrinfeld.Differentiation.fiberEval_spec line 1566
  282. theorem OAI.DeligneDrinfeld.Differentiation.fiberEval_base line 1574
  283. theorem OAI.DeligneDrinfeld.Differentiation.fiberEval_Fb line 1582
  284. theorem OAI.DeligneDrinfeld.Differentiation.transverse line 1587
  285. theorem OAI.DeligneDrinfeld.Differentiation.slope_G_formula line 1633
  286. def OAI.DeligneDrinfeld.Differentiation.swapJet line 1643
  287. theorem OAI.DeligneDrinfeld.Differentiation.mixed_slope line 1652
  288. theorem OAI.DeligneDrinfeld.Differentiation.adPower_base line 1659
  289. theorem OAI.DeligneDrinfeld.Differentiation.adPower_radial line 1663
  290. theorem OAI.DeligneDrinfeld.Differentiation.adPower_transverse_self line 1673
  291. theorem OAI.DeligneDrinfeld.Differentiation.adPower_zero_base line 1687
  292. theorem OAI.DeligneDrinfeld.Differentiation.mixed_scalar line 1695
  293. theorem OAI.DeligneDrinfeld.Differentiation.diagonal_scalar_zero line 1720
  294. theorem OAI.DeligneDrinfeld.Differentiation.special_linearization line 1739
  295. theorem OAI.DeligneDrinfeld.Differentiation.special_G_zero line 1747
  296. theorem OAI.DeligneDrinfeld.Differentiation.special_identity line 1771
  297. abbrev OAI.DeligneDrinfeld.Elimination.F line 1781
  298. abbrev OAI.DeligneDrinfeld.Elimination.G line 1782
  299. def OAI.DeligneDrinfeld.Elimination.X line 1783
  300. def OAI.DeligneDrinfeld.Elimination.Y line 1784
  301. def OAI.DeligneDrinfeld.Elimination.E line 1785
  302. def OAI.DeligneDrinfeld.Elimination.shift line 1786
  303. theorem OAI.DeligneDrinfeld.Elimination.shift_E line 1788
  304. def OAI.DeligneDrinfeld.Elimination.action line 1790
  305. abbrev OAI.DeligneDrinfeld.Elimination.M line 1795
  306. def OAI.DeligneDrinfeld.Elimination.expand line 1797
  307. theorem OAI.DeligneDrinfeld.Elimination.expand_X line 1801
  308. theorem OAI.DeligneDrinfeld.Elimination.expand_Y line 1803
  309. def OAI.DeligneDrinfeld.Elimination.adWord line 1806
  310. theorem OAI.DeligneDrinfeld.Elimination.adWord_zero line 1808
  311. theorem OAI.DeligneDrinfeld.Elimination.adWord_succ line 1809
  312. def OAI.DeligneDrinfeld.Elimination.collapseFiber line 1812
  313. theorem OAI.DeligneDrinfeld.Elimination.collapseFiber_E line 1813
  314. theorem OAI.DeligneDrinfeld.Elimination.collapse_shift line 1816
  315. def OAI.DeligneDrinfeld.Elimination.scalarX line 1826
  316. def OAI.DeligneDrinfeld.Elimination.collapse line 1832
  317. theorem OAI.DeligneDrinfeld.Elimination.collapse_inl line 1838
  318. theorem OAI.DeligneDrinfeld.Elimination.collapse_inr line 1840
  319. theorem OAI.DeligneDrinfeld.Elimination.collapse_expand line 1843
  320. theorem OAI.DeligneDrinfeld.Elimination.expand_adWord line 1850
  321. theorem OAI.DeligneDrinfeld.Elimination.expand_collapseFiber line 1859
  322. theorem OAI.DeligneDrinfeld.Elimination.expand_collapse line 1868
  323. def OAI.DeligneDrinfeld.Elimination.equivalence line 1875
  324. theorem OAI.DeligneDrinfeld.Elimination.collapseFiber_injective line 1881
  325. abbrev OAI.DeligneDrinfeld.AssociativeElimination.A line 1893
  326. def OAI.DeligneDrinfeld.AssociativeElimination.atom line 1894
  327. def OAI.DeligneDrinfeld.AssociativeElimination.lift line 1896
  328. theorem OAI.DeligneDrinfeld.AssociativeElimination.lift_atom line 1898
  329. theorem OAI.DeligneDrinfeld.AssociativeElimination.hom_ext line 1901
  330. def OAI.DeligneDrinfeld.AssociativeElimination.embed line 1908
  331. theorem OAI.DeligneDrinfeld.AssociativeElimination.embed_of line 1909
  332. def OAI.DeligneDrinfeld.AssociativeElimination.dualLift line 1911
  333. theorem OAI.DeligneDrinfeld.AssociativeElimination.dualLift_base line 1913
  334. def OAI.DeligneDrinfeld.AssociativeElimination.deriv line 1921
  335. theorem OAI.DeligneDrinfeld.AssociativeElimination.deriv_atom line 1923
  336. theorem OAI.DeligneDrinfeld.AssociativeElimination.deriv_one line 1925
  337. theorem OAI.DeligneDrinfeld.AssociativeElimination.deriv_mul line 1926
  338. theorem OAI.DeligneDrinfeld.AssociativeElimination.deriv_lie line 1931
  339. def OAI.DeligneDrinfeld.AssociativeElimination.shift line 1936
  340. theorem OAI.DeligneDrinfeld.AssociativeElimination.shift_atom line 1937
  341. theorem OAI.DeligneDrinfeld.AssociativeElimination.shift_one line 1939
  342. theorem OAI.DeligneDrinfeld.AssociativeElimination.shift_mul line 1940
  343. theorem OAI.DeligneDrinfeld.AssociativeElimination.embed_shift line 1942
  344. def OAI.DeligneDrinfeld.AssociativeElimination.leftMul line 1952
  345. theorem OAI.DeligneDrinfeld.AssociativeElimination.leftMul_apply line 1953
  346. theorem OAI.DeligneDrinfeld.AssociativeElimination.comm_shift_left line 1954
  347. def OAI.DeligneDrinfeld.AssociativeElimination.scalarShift line 1961
  348. def OAI.DeligneDrinfeld.AssociativeElimination.representation line 1967
  349. def OAI.DeligneDrinfeld.AssociativeElimination.operator line 1977
  350. theorem OAI.DeligneDrinfeld.AssociativeElimination.representation_inl line 1980
  351. theorem OAI.DeligneDrinfeld.AssociativeElimination.representation_inr line 1982
  352. theorem OAI.DeligneDrinfeld.AssociativeElimination.operator_embed line 1986
  353. def OAI.DeligneDrinfeld.AssociativeElimination.extract line 1994
  354. theorem OAI.DeligneDrinfeld.AssociativeElimination.extract_embed line 1997
  355. abbrev OAI.DeligneDrinfeld.IntegralWords.AQ line 2011
  356. def OAI.DeligneDrinfeld.IntegralWords.word line 2013
  357. theorem OAI.DeligneDrinfeld.IntegralWords.word_nil line 2014
  358. theorem OAI.DeligneDrinfeld.IntegralWords.word_singleton line 2015
  359. theorem OAI.DeligneDrinfeld.IntegralWords.word_append line 2016
  360. theorem OAI.DeligneDrinfeld.IntegralWords.word_cons line 2018
  361. def OAI.DeligneDrinfeld.IntegralWords.lattice line 2021
  362. def OAI.DeligneDrinfeld.IntegralWords.lieLattice line 2022
  363. def OAI.DeligneDrinfeld.IntegralWords.rationalLie line 2023
  364. theorem OAI.DeligneDrinfeld.IntegralWords.word_integral line 2025
  365. theorem OAI.DeligneDrinfeld.IntegralWords.atom_integral line 2026
  366. theorem OAI.DeligneDrinfeld.IntegralWords.one_integral line 2027
  367. theorem OAI.DeligneDrinfeld.IntegralWords.integral_mul line 2029
  368. theorem OAI.DeligneDrinfeld.IntegralWords.integral_lie line 2045
  369. theorem OAI.DeligneDrinfeld.IntegralWords.integral_coeff line 2048
  370. theorem OAI.DeligneDrinfeld.IntegralWords.integral_of_coeff line 2069
  371. def OAI.DeligneDrinfeld.IntegralWords.words line 2079
  372. theorem OAI.DeligneDrinfeld.IntegralWords.word_mem line 2082
  373. theorem OAI.DeligneDrinfeld.IntegralWords.mem_words line 2085
  374. theorem OAI.DeligneDrinfeld.IntegralWords.words_mono line 2112
  375. theorem OAI.DeligneDrinfeld.IntegralWords.mul_words line 2117
  376. theorem OAI.DeligneDrinfeld.IntegralWords.lie_has_preimage line 2134
  377. theorem OAI.DeligneDrinfeld.IntegralWords.embed_mem_lie line 2141
  378. theorem OAI.DeligneDrinfeld.IntegralWords.shift_integral line 2149
  379. theorem OAI.DeligneDrinfeld.IntegralWords.extract_integral line 2165
  380. theorem OAI.DeligneDrinfeld.IntegralWords.extract_lie line 2182
  381. def OAI.DeligneDrinfeld.IntegralWords.countSome line 2187
  382. theorem OAI.DeligneDrinfeld.IntegralWords.countSome_le line 2192
  383. theorem OAI.DeligneDrinfeld.IntegralWords.countSome_lt line 2197
  384. theorem OAI.DeligneDrinfeld.IntegralWords.shift_length line 2208
  385. theorem OAI.DeligneDrinfeld.IntegralWords.operator_length line 2228
  386. theorem OAI.DeligneDrinfeld.IntegralWords.extract_word_length line 2244
  387. def OAI.DeligneDrinfeld.IntegralWords.rename line 2248
  388. theorem OAI.DeligneDrinfeld.IntegralWords.rename_atom line 2249
  389. theorem OAI.DeligneDrinfeld.IntegralWords.rename_word line 2252
  390. theorem OAI.DeligneDrinfeld.IntegralWords.rename_integral line 2257
  391. theorem OAI.DeligneDrinfeld.IntegralWords.rename_lie line 2264
  392. theorem OAI.DeligneDrinfeld.IntegralWords.rename_lieIntegral line 2272
  393. def OAI.DeligneDrinfeld.IntegralWords.kill line 2280
  394. theorem OAI.DeligneDrinfeld.IntegralWords.kill_atom line 2284
  395. theorem OAI.DeligneDrinfeld.IntegralWords.kill_word line 2288
  396. theorem OAI.DeligneDrinfeld.IntegralWords.kill_integral line 2296
  397. theorem OAI.DeligneDrinfeld.IntegralWords.kill_lie line 2307
  398. def OAI.DeligneDrinfeld.IntegralWords.tag line 2321
  399. def OAI.DeligneDrinfeld.IntegralWords.untag line 2323
  400. theorem OAI.DeligneDrinfeld.IntegralWords.rename_untag_tag line 2327
  401. theorem OAI.DeligneDrinfeld.IntegralWords.rename_extract_lower line 2339
  402. theorem OAI.DeligneDrinfeld.IntegralWords.kill_bound line 2356
  403. theorem OAI.DeligneDrinfeld.IntegralWords.remainder_bound line 2375
  404. theorem OAI.DeligneDrinfeld.IntegralWords.lie_positive line 2392
  405. def OAI.DeligneDrinfeld.IntegralWords.traceX line 2403
  406. theorem OAI.DeligneDrinfeld.IntegralWords.trace_embed line 2405
  407. def OAI.DeligneDrinfeld.IntegralWords.collapseAssoc line 2413
  408. theorem OAI.DeligneDrinfeld.IntegralWords.collapse_embed line 2416
  409. theorem OAI.DeligneDrinfeld.IntegralWords.decompose_lie line 2426
  410. theorem OAI.DeligneDrinfeld.IntegralWords.trace_integral line 2435
  411. theorem OAI.DeligneDrinfeld.IntegralWords.adWord_integralLie line 2459
  412. theorem OAI.DeligneDrinfeld.IntegralWords.collapse_integralLie line 2471
  413. theorem OAI.DeligneDrinfeld.IntegralWords.words_and line 2481
  414. theorem OAI.DeligneDrinfeld.IntegralWords.exists_support line 2487
  415. theorem OAI.DeligneDrinfeld.IntegralWords.exists_bound line 2493
  416. theorem OAI.DeligneDrinfeld.IntegralWords.bound_zero_of_lie line 2498
  417. theorem OAI.DeligneDrinfeld.IntegralWords.support_empty_of_lie line 2507
  418. theorem OAI.DeligneDrinfeld.IntegralWords.saturation_bounded line 2522
  419. theorem OAI.DeligneDrinfeld.IntegralWords.saturation line 2566
  420. abbrev OAI.DeligneDrinfeld.UniversalEmbedding.FL line 2576
  421. inductive OAI.DeligneDrinfeld.UniversalEmbedding.Tree line 2578
  422. def OAI.DeligneDrinfeld.UniversalEmbedding.Tree.leaves line 2582
  423. def OAI.DeligneDrinfeld.UniversalEmbedding.Tree.eval line 2586
  424. def OAI.DeligneDrinfeld.UniversalEmbedding.Tree.map line 2590
  425. theorem OAI.DeligneDrinfeld.UniversalEmbedding.Tree.leaves_map line 2594
  426. theorem OAI.DeligneDrinfeld.UniversalEmbedding.Tree.positive line 2598
  427. def OAI.DeligneDrinfeld.UniversalEmbedding.bounded line 2601
  428. def OAI.DeligneDrinfeld.UniversalEmbedding.small line 2603
  429. theorem OAI.DeligneDrinfeld.UniversalEmbedding.eval_bounded line 2606
  430. theorem OAI.DeligneDrinfeld.UniversalEmbedding.eval_small line 2609
  431. theorem OAI.DeligneDrinfeld.UniversalEmbedding.bounded_mono line 2612
  432. theorem OAI.DeligneDrinfeld.UniversalEmbedding.bounded_small line 2617
  433. theorem OAI.DeligneDrinfeld.UniversalEmbedding.small_mono line 2623
  434. theorem OAI.DeligneDrinfeld.UniversalEmbedding.bracket_small line 2629
  435. theorem OAI.DeligneDrinfeld.UniversalEmbedding.small_exists_support line 2645
  436. theorem OAI.DeligneDrinfeld.UniversalEmbedding.small_exists line 2662
  437. theorem OAI.DeligneDrinfeld.UniversalEmbedding.small_zero line 2677
  438. theorem OAI.DeligneDrinfeld.UniversalEmbedding.bounded_empty line 2685
  439. def OAI.DeligneDrinfeld.UniversalEmbedding.rename line 2693
  440. def OAI.DeligneDrinfeld.UniversalEmbedding.renameAssoc line 2695
  441. theorem OAI.DeligneDrinfeld.UniversalEmbedding.rename_of line 2696
  442. theorem OAI.DeligneDrinfeld.UniversalEmbedding.rename_eval line 2698
  443. theorem OAI.DeligneDrinfeld.UniversalEmbedding.rename_embed line 2702
  444. def OAI.DeligneDrinfeld.UniversalEmbedding.kill line 2711
  445. def OAI.DeligneDrinfeld.UniversalEmbedding.killAssoc line 2713
  446. theorem OAI.DeligneDrinfeld.UniversalEmbedding.kill_of line 2715
  447. theorem OAI.DeligneDrinfeld.UniversalEmbedding.kill_embed line 2718
  448. theorem OAI.DeligneDrinfeld.UniversalEmbedding.kill_eval line 2726
  449. theorem OAI.DeligneDrinfeld.UniversalEmbedding.kill_bounded line 2734
  450. def OAI.DeligneDrinfeld.UniversalEmbedding.fiber line 2748
  451. theorem OAI.DeligneDrinfeld.UniversalEmbedding.fiber_X line 2753
  452. theorem OAI.DeligneDrinfeld.UniversalEmbedding.fiber_Y line 2755
  453. theorem OAI.DeligneDrinfeld.UniversalEmbedding.fiber_lie line 2757
  454. theorem OAI.DeligneDrinfeld.UniversalEmbedding.shift_small line 2762
  455. theorem OAI.DeligneDrinfeld.UniversalEmbedding.countSome_append line 2781
  456. theorem OAI.DeligneDrinfeld.UniversalEmbedding.fiber_eval line 2789
  457. theorem OAI.DeligneDrinfeld.UniversalEmbedding.fiber_remainder line 2808
  458. def OAI.DeligneDrinfeld.UniversalEmbedding.traceAssoc line 2832
  459. theorem OAI.DeligneDrinfeld.UniversalEmbedding.trace_embed line 2833
  460. theorem OAI.DeligneDrinfeld.UniversalEmbedding.untag_tag line 2842
  461. theorem OAI.DeligneDrinfeld.UniversalEmbedding.kernel_bounded line 2854
  462. theorem OAI.DeligneDrinfeld.UniversalEmbedding.injective line 2885
  463. abbrev OAI.DeligneDrinfeld.QuadraticAlphabet.F line 2896
  464. inductive OAI.DeligneDrinfeld.QuadraticAlphabet.Letter line 2897
  465. instance OAI.DeligneDrinfeld.QuadraticAlphabet.(instance at line 2898) line 2898
  466. abbrev OAI.DeligneDrinfeld.QuadraticAlphabet.S line 2900
  467. abbrev OAI.DeligneDrinfeld.QuadraticAlphabet.T line 2901
  468. def OAI.DeligneDrinfeld.QuadraticAlphabet.a line 2902
  469. def OAI.DeligneDrinfeld.QuadraticAlphabet.c line 2903
  470. def OAI.DeligneDrinfeld.QuadraticAlphabet.b line 2904
  471. def OAI.DeligneDrinfeld.QuadraticAlphabet.x line 2905
  472. def OAI.DeligneDrinfeld.QuadraticAlphabet.y line 2906
  473. def OAI.DeligneDrinfeld.QuadraticAlphabet.delta line 2908
  474. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_a line 2909
  475. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_b line 2910
  476. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_c line 2911
  477. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_one line 2912
  478. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_mul line 2913
  479. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_lie line 2914
  480. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.algebra_induction line 2916
  481. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_square_mul line 2933
  482. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.delta_square line 2940
  483. def OAI.DeligneDrinfeld.QuadraticAlphabet.left line 2952
  484. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.left_apply line 2963
  485. def OAI.DeligneDrinfeld.QuadraticAlphabet.root line 2965
  486. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.root_apply line 2969
  487. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.root_comm line 2971
  488. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.root_square line 2976
  489. def OAI.DeligneDrinfeld.QuadraticAlphabet.substitution line 2988
  490. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.substitution_a line 2989
  491. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.substitution_c line 2990
  492. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.substitution_b line 2991
  493. def OAI.DeligneDrinfeld.QuadraticAlphabet.representation line 2993
  494. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.representation_x line 2995
  495. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.representation_y line 2996
  496. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.representation_substitution line 2998
  497. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.left_injective line 3012
  498. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.substitution_injective line 3017
  499. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.ad_square line 3023
  500. abbrev OAI.DeligneDrinfeld.QuadraticAlphabet.LABC line 3029
  501. def OAI.DeligneDrinfeld.QuadraticAlphabet.la line 3030
  502. def OAI.DeligneDrinfeld.QuadraticAlphabet.lc line 3031
  503. def OAI.DeligneDrinfeld.QuadraticAlphabet.lb line 3032
  504. def OAI.DeligneDrinfeld.QuadraticAlphabet.under line 3033
  505. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.under_a line 3034
  506. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.under_c line 3035
  507. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.under_b line 3036
  508. def OAI.DeligneDrinfeld.QuadraticAlphabet.lieDelta line 3038
  509. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.lieDelta_a line 3040
  510. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.lieDelta_c line 3041
  511. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.lieDelta_b line 3042
  512. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.under_delta line 3044
  513. def OAI.DeligneDrinfeld.QuadraticAlphabet.iter line 3058
  514. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.iter_zero line 3059
  515. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.iter_succ line 3060
  516. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.under_iter line 3063
  517. def OAI.DeligneDrinfeld.QuadraticAlphabet.fiberLift line 3070
  518. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.under_fiberLift line 3072
  519. def OAI.DeligneDrinfeld.QuadraticAlphabet.polynomial line 3081
  520. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.decompose line 3083
  521. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.under_injective line 3091
  522. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.represent_unique line 3095
  523. def OAI.DeligneDrinfeld.QuadraticAlphabet.homogeneous line 3103
  524. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.homogeneous_trace_zero line 3106
  525. theorem OAI.DeligneDrinfeld.QuadraticAlphabet.homogeneous_representation line 3121
  526. def OAI.DeligneDrinfeld.AssociativeDerivations.extend line 3133
  527. theorem OAI.DeligneDrinfeld.AssociativeDerivations.extend_atom line 3135
  528. theorem OAI.DeligneDrinfeld.AssociativeDerivations.extend_one line 3137
  529. theorem OAI.DeligneDrinfeld.AssociativeDerivations.extend_mul line 3139
  530. theorem OAI.DeligneDrinfeld.AssociativeDerivations.extend_embed line 3142
  531. theorem OAI.DeligneDrinfeld.AssociativeDerivations.linear_ext line 3154
  532. theorem OAI.DeligneDrinfeld.AssociativeDerivations.comm_mul line 3167
  533. def OAI.DeligneDrinfeld.AssociativeDerivations.hom line 3175
  534. theorem OAI.DeligneDrinfeld.AssociativeDerivations.hom_apply line 3199
  535. theorem OAI.DeligneDrinfeld.AssociativeDerivations.comm_left line 3202
  536. theorem OAI.DeligneDrinfeld.EnvelopingTools.induction line 3215
  537. abbrev OAI.DeligneDrinfeld.FiberPBW.M line 3251
  538. def OAI.DeligneDrinfeld.FiberPBW.onLeft line 3254
  539. def OAI.DeligneDrinfeld.FiberPBW.onRight line 3257
  540. theorem OAI.DeligneDrinfeld.FiberPBW.onLeft_tmul line 3260
  541. theorem OAI.DeligneDrinfeld.FiberPBW.onRight_tmul line 3262
  542. theorem OAI.DeligneDrinfeld.FiberPBW.commute_tensor line 3265
  543. def OAI.DeligneDrinfeld.FiberPBW.fiber line 3271
  544. def OAI.DeligneDrinfeld.FiberPBW.action line 3274
  545. def OAI.DeligneDrinfeld.FiberPBW.baseLeft line 3277
  546. def OAI.DeligneDrinfeld.FiberPBW.constant line 3279
  547. def OAI.DeligneDrinfeld.FiberPBW.base line 3283
  548. theorem OAI.DeligneDrinfeld.FiberPBW.fiber_tmul line 3306
  549. theorem OAI.DeligneDrinfeld.FiberPBW.base_tmul line 3308
  550. theorem OAI.DeligneDrinfeld.FiberPBW.compatibility line 3312
  551. def OAI.DeligneDrinfeld.FiberPBW.representation line 3322
  552. def OAI.DeligneDrinfeld.FiberPBW.operators line 3325
  553. def OAI.DeligneDrinfeld.FiberPBW.fiberIn line 3328
  554. def OAI.DeligneDrinfeld.FiberPBW.baseIn line 3330
  555. theorem OAI.DeligneDrinfeld.FiberPBW.operators_fiber line 3333
  556. theorem OAI.DeligneDrinfeld.FiberPBW.operators_base_one line 3341
  557. def OAI.DeligneDrinfeld.FiberPBW.normal line 3354
  558. theorem OAI.DeligneDrinfeld.FiberPBW.normal_tmul line 3362
  559. def OAI.DeligneDrinfeld.FiberPBW.extract line 3365
  560. theorem OAI.DeligneDrinfeld.FiberPBW.extract_normal line 3368
  561. theorem OAI.DeligneDrinfeld.FiberPBW.normal_injective line 3382
  562. abbrev OAI.DeligneDrinfeld.GenericBraid.Free line 3390
  563. def OAI.DeligneDrinfeld.GenericBraid.gen line 3391
  564. def OAI.DeligneDrinfeld.GenericBraid.relations line 3392
  565. def OAI.DeligneDrinfeld.GenericBraid.ideal line 3396
  566. abbrev OAI.DeligneDrinfeld.GenericBraid.T line 3397
  567. def OAI.DeligneDrinfeld.GenericBraid.t line 3398
  568. theorem OAI.DeligneDrinfeld.GenericBraid.relation_zero line 3400
  569. theorem OAI.DeligneDrinfeld.GenericBraid.t_self line 3403
  570. theorem OAI.DeligneDrinfeld.GenericBraid.t_comm line 3405
  571. theorem OAI.DeligneDrinfeld.GenericBraid.t_disjoint line 3408
  572. theorem OAI.DeligneDrinfeld.GenericBraid.t_three line 3412
  573. def OAI.DeligneDrinfeld.GenericBraid.lift line 3418
  574. theorem OAI.DeligneDrinfeld.GenericBraid.lift_t line 3437
  575. def OAI.DeligneDrinfeld.GenericBraid.action line 3443
  576. theorem OAI.DeligneDrinfeld.GenericBraid.action_t line 3447
  577. def OAI.DeligneDrinfeld.GenericBraid.fiber line 3448
  578. def OAI.DeligneDrinfeld.GenericBraid.base line 3449
  579. def OAI.DeligneDrinfeld.GenericBraid.chord line 3450
  580. theorem OAI.DeligneDrinfeld.GenericBraid.chord_nn line 3455
  581. theorem OAI.DeligneDrinfeld.GenericBraid.chord_ns line 3456
  582. theorem OAI.DeligneDrinfeld.GenericBraid.chord_sn line 3457
  583. theorem OAI.DeligneDrinfeld.GenericBraid.chord_ss line 3458
  584. theorem OAI.DeligneDrinfeld.GenericBraid.chord_self line 3459
  585. theorem OAI.DeligneDrinfeld.GenericBraid.chord_comm line 3461
  586. theorem OAI.DeligneDrinfeld.GenericBraid.base_fiber line 3463
  587. theorem OAI.DeligneDrinfeld.GenericBraid.fiber_base line 3466
  588. theorem OAI.DeligneDrinfeld.GenericBraid.chord_disjoint line 3469
  589. theorem OAI.DeligneDrinfeld.GenericBraid.chord_three line 3475
  590. def OAI.DeligneDrinfeld.GenericBraid.toSemidirect line 3507
  591. theorem OAI.DeligneDrinfeld.GenericBraid.toSemidirect_t line 3509
  592. abbrev OAI.DeligneDrinfeld.RestrictedAlphabet.F line 3516
  593. inductive OAI.DeligneDrinfeld.RestrictedAlphabet.Letter line 3517
  594. abbrev OAI.DeligneDrinfeld.RestrictedAlphabet.S line 3519
  595. abbrev OAI.DeligneDrinfeld.RestrictedAlphabet.T line 3520
  596. def OAI.DeligneDrinfeld.RestrictedAlphabet.a line 3521
  597. def OAI.DeligneDrinfeld.RestrictedAlphabet.b line 3522
  598. def OAI.DeligneDrinfeld.RestrictedAlphabet.c line 3523
  599. def OAI.DeligneDrinfeld.RestrictedAlphabet.y line 3524
  600. def OAI.DeligneDrinfeld.RestrictedAlphabet.x line 3525
  601. def OAI.DeligneDrinfeld.RestrictedAlphabet.delta line 3526
  602. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_a line 3527
  603. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_b line 3528
  604. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_c line 3529
  605. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_one line 3530
  606. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_mul line 3531
  607. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_lie line 3532
  608. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_square_mul line 3533
  609. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.delta_square line 3539
  610. def OAI.DeligneDrinfeld.RestrictedAlphabet.left line 3551
  611. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.left_apply line 3561
  612. def OAI.DeligneDrinfeld.RestrictedAlphabet.root line 3563
  613. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.root_apply line 3567
  614. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.root_comm line 3568
  615. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.root_square line 3572
  616. def OAI.DeligneDrinfeld.RestrictedAlphabet.substitution line 3584
  617. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.substitution_a line 3585
  618. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.substitution_c line 3586
  619. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.substitution_b line 3587
  620. def OAI.DeligneDrinfeld.RestrictedAlphabet.representation line 3588
  621. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.representation_x line 3590
  622. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.representation_y line 3591
  623. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.representation_substitution line 3592
  624. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.injective line 3605
  625. abbrev OAI.DeligneDrinfeld.GenericBraid.Env line 3619
  626. def OAI.DeligneDrinfeld.GenericBraid.baseLie line 3621
  627. theorem OAI.DeligneDrinfeld.GenericBraid.baseLie_t line 3630
  628. theorem OAI.DeligneDrinfeld.GenericBraid.hom_ext line 3634
  629. def OAI.DeligneDrinfeld.GenericBraid.fiberIn line 3647
  630. def OAI.DeligneDrinfeld.GenericBraid.baseIn line 3649
  631. def OAI.DeligneDrinfeld.GenericBraid.toSemi line 3651
  632. theorem OAI.DeligneDrinfeld.GenericBraid.toSemi_fiber line 3655
  633. theorem OAI.DeligneDrinfeld.GenericBraid.toSemi_base line 3660
  634. def OAI.DeligneDrinfeld.GenericBraid.normal line 3666
  635. theorem OAI.DeligneDrinfeld.GenericBraid.normal_tmul line 3675
  636. theorem OAI.DeligneDrinfeld.GenericBraid.toSemi_normal line 3678
  637. theorem OAI.DeligneDrinfeld.GenericBraid.normal_injective line 3688
  638. def OAI.DeligneDrinfeld.RestrictedAlphabet.normal line 3702
  639. theorem OAI.DeligneDrinfeld.RestrictedAlphabet.normal_injective line 3706
  640. def OAI.DeligneDrinfeld.Deletion.word line 3717
  641. theorem OAI.DeligneDrinfeld.Deletion.word_nil line 3718
  642. theorem OAI.DeligneDrinfeld.Deletion.word_cons line 3719
  643. def OAI.DeligneDrinfeld.Deletion.raw line 3722
  644. def OAI.DeligneDrinfeld.Deletion.op line 3726
  645. theorem OAI.DeligneDrinfeld.Deletion.op_word line 3729
  646. theorem OAI.DeligneDrinfeld.Deletion.op_one line 3732
  647. theorem OAI.DeligneDrinfeld.Deletion.op_cons line 3734
  648. theorem OAI.DeligneDrinfeld.Deletion.op_mul_word line 3737
  649. theorem OAI.DeligneDrinfeld.Deletion.op_two line 3741
  650. def OAI.DeligneDrinfeld.Deletion.curvature line 3751
  651. theorem OAI.DeligneDrinfeld.Deletion.comm_cons line 3755
  652. theorem OAI.DeligneDrinfeld.Deletion.commute_of_curvature line 3763
  653. theorem OAI.DeligneDrinfeld.Deletion.linear_ext line 3788
  654. theorem OAI.DeligneDrinfeld.Deletion.raw_add line 3797
  655. theorem OAI.DeligneDrinfeld.Deletion.op_add line 3802
  656. theorem OAI.DeligneDrinfeld.Deletion.op_zero line 3807
  657. theorem OAI.DeligneDrinfeld.Deletion.op_list_sum line 3815
  658. inductive OAI.DeligneDrinfeld.DeletionTable.Letter line 3825
  659. instance OAI.DeligneDrinfeld.DeletionTable.(instance at line 3826) line 3826
  660. inductive OAI.DeligneDrinfeld.DeletionTable.Hyperplane line 3827
  661. instance OAI.DeligneDrinfeld.DeletionTable.(instance at line 3828) line 3828
  662. def OAI.DeligneDrinfeld.DeletionTable.weight line 3831
  663. def OAI.DeligneDrinfeld.DeletionTable.flat line 3846
  664. def OAI.DeligneDrinfeld.DeletionTable.total line 3861
  665. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_0 line 3863
  666. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_1 line 3866
  667. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_2 line 3869
  668. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_3 line 3872
  669. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_4 line 3875
  670. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_5 line 3878
  671. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_6 line 3881
  672. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_7 line 3884
  673. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_8 line 3887
  674. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_9 line 3890
  675. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_10 line 3893
  676. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_11 line 3896
  677. theorem OAI.DeligneDrinfeld.DeletionTable.curvature_12 line 3899
  678. theorem OAI.DeligneDrinfeld.DeletionTable.flat_curvature line 3902
  679. theorem OAI.DeligneDrinfeld.DeletionTable.integral_flat line 3919
  680. theorem OAI.DeligneDrinfeld.GenericBraid.induction line 3931
  681. def OAI.DeligneDrinfeld.GenericBraid.fiberLie line 3943
  682. theorem OAI.DeligneDrinfeld.GenericBraid.fiberLie_of line 3946
  683. theorem OAI.DeligneDrinfeld.GenericBraid.t_base_fiber_left line 3949
  684. theorem OAI.DeligneDrinfeld.GenericBraid.compatibility line 3958
  685. def OAI.DeligneDrinfeld.GenericBraid.fromSemidirect line 3988
  686. theorem OAI.DeligneDrinfeld.GenericBraid.toSemidirect_fiberLie line 3991
  687. theorem OAI.DeligneDrinfeld.GenericBraid.toSemidirect_baseLie line 3999
  688. theorem OAI.DeligneDrinfeld.GenericBraid.to_from line 4007
  689. theorem OAI.DeligneDrinfeld.GenericBraid.from_to line 4013
  690. def OAI.DeligneDrinfeld.GenericBraid.equivalence line 4020
  691. def OAI.DeligneDrinfeld.IntegralBaseChange.words line 4033
  692. theorem OAI.DeligneDrinfeld.IntegralBaseChange.words_atom line 4034
  693. theorem OAI.DeligneDrinfeld.IntegralBaseChange.words_coeff line 4036
  694. def OAI.DeligneDrinfeld.IntegralBaseChange.lie line 4038
  695. theorem OAI.DeligneDrinfeld.IntegralBaseChange.lie_of line 4040
  696. theorem OAI.DeligneDrinfeld.IntegralBaseChange.embed_lie line 4041
  697. theorem OAI.DeligneDrinfeld.IntegralBaseChange.words_rational_injective line 4049
  698. theorem OAI.DeligneDrinfeld.IntegralBaseChange.lie_rational_injective line 4055
  699. theorem OAI.DeligneDrinfeld.IntegralBaseChange.lift_integral line 4061
  700. def OAI.DeligneDrinfeld.GenericBraid.cast line 4094
  701. theorem OAI.DeligneDrinfeld.GenericBraid.cast_t line 4096
  702. def OAI.DeligneDrinfeld.GenericBraid.rename line 4097
  703. theorem OAI.DeligneDrinfeld.GenericBraid.rename_t line 4102
  704. theorem OAI.DeligneDrinfeld.GenericBraid.rename_symm line 4104
  705. theorem OAI.DeligneDrinfeld.GenericBraid.rename_injective line 4112
  706. theorem OAI.DeligneDrinfeld.GenericBraid.cast_rename line 4114
  707. theorem OAI.DeligneDrinfeld.GenericBraid.cast_fiber line 4124
  708. theorem OAI.DeligneDrinfeld.GenericBraid.cast_base line 4133
  709. theorem OAI.DeligneDrinfeld.GenericBraid.cast_option_injective line 4140
  710. theorem OAI.DeligneDrinfeld.GenericBraid.cast_fin_injective line 4158
  711. theorem OAI.DeligneDrinfeld.GenericBraid.cast_finite_injective line 4175
  712. def OAI.DeligneDrinfeld.GenericBraid.fromT4 line 4181
  713. theorem OAI.DeligneDrinfeld.GenericBraid.fromT4_t line 4184
  714. def OAI.DeligneDrinfeld.BaseChangeEquations.x line 4190
  715. def OAI.DeligneDrinfeld.BaseChangeEquations.y line 4191
  716. def OAI.DeligneDrinfeld.BaseChangeEquations.eval line 4192
  717. theorem OAI.DeligneDrinfeld.BaseChangeEquations.eval_x line 4194
  718. theorem OAI.DeligneDrinfeld.BaseChangeEquations.eval_y line 4195
  719. def OAI.DeligneDrinfeld.BaseChangeEquations.antisymmetry line 4196
  720. def OAI.DeligneDrinfeld.BaseChangeEquations.threeTerm line 4197
  721. def OAI.DeligneDrinfeld.BaseChangeEquations.pentagon line 4198
  722. def OAI.DeligneDrinfeld.BaseChangeEquations.Equations line 4203
  723. theorem OAI.DeligneDrinfeld.BaseChangeEquations.pentagon_rational line 4206
  724. theorem OAI.DeligneDrinfeld.BaseChangeEquations.rational line 4221
  725. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_eval_lie line 4225
  726. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_eval_braid line 4236
  727. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_x line 4245
  728. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_y line 4246
  729. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_antisymmetry line 4247
  730. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_threeTerm line 4250
  731. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_pentagon line 4253
  732. theorem OAI.DeligneDrinfeld.BaseChangeEquations.integral_of_rational line 4257
  733. theorem OAI.DeligneDrinfeld.BaseChangeEquations.reduce line 4266
  734. abbrev OAI.DeligneDrinfeld.PolynomialOrdering.V line 4280
  735. def OAI.DeligneDrinfeld.PolynomialOrdering.fiberOp line 4282
  736. def OAI.DeligneDrinfeld.PolynomialOrdering.baseOp line 4284
  737. def OAI.DeligneDrinfeld.PolynomialOrdering.op line 4287
  738. theorem OAI.DeligneDrinfeld.PolynomialOrdering.fiberOp_tmul line 4289
  739. theorem OAI.DeligneDrinfeld.PolynomialOrdering.baseOp_tmul line 4291
  740. def OAI.DeligneDrinfeld.PolynomialOrdering.operators line 4294
  741. def OAI.DeligneDrinfeld.PolynomialOrdering.normalize line 4296
  742. theorem OAI.DeligneDrinfeld.PolynomialOrdering.normalize_one line 4298
  743. theorem OAI.DeligneDrinfeld.PolynomialOrdering.normalize_atom_mul line 4300
  744. def OAI.DeligneDrinfeld.PolynomialOrdering.interpret line 4308
  745. theorem OAI.DeligneDrinfeld.PolynomialOrdering.interpret_tmul line 4316
  746. def OAI.DeligneDrinfeld.PolynomialOrdering.evaluate line 4319
  747. theorem OAI.DeligneDrinfeld.PolynomialOrdering.commutator line 4325
  748. theorem OAI.DeligneDrinfeld.PolynomialOrdering.interpret_op line 4336
  749. theorem OAI.DeligneDrinfeld.PolynomialOrdering.interpret_operators line 4352
  750. theorem OAI.DeligneDrinfeld.PolynomialOrdering.interpret_normalize line 4361
  751. def OAI.DeligneDrinfeld.PolynomialOrdering.fiberIn line 4367
  752. def OAI.DeligneDrinfeld.PolynomialOrdering.baseIn line 4368
  753. theorem OAI.DeligneDrinfeld.PolynomialOrdering.operators_fiber line 4369
  754. theorem OAI.DeligneDrinfeld.PolynomialOrdering.operators_base_one line 4376
  755. theorem OAI.DeligneDrinfeld.PolynomialOrdering.normalize_product line 4387
  756. def OAI.DeligneDrinfeld.WordGrading.word line 4401
  757. theorem OAI.DeligneDrinfeld.WordGrading.word_one line 4402
  758. theorem OAI.DeligneDrinfeld.WordGrading.word_of line 4403
  759. theorem OAI.DeligneDrinfeld.WordGrading.word_mul line 4404
  760. def OAI.DeligneDrinfeld.WordGrading.space line 4406
  761. theorem OAI.DeligneDrinfeld.WordGrading.word_mem line 4408
  762. theorem OAI.DeligneDrinfeld.WordGrading.space_mono line 4410
  763. theorem OAI.DeligneDrinfeld.WordGrading.coeff_support line 4415
  764. theorem OAI.DeligneDrinfeld.WordGrading.mem_space line 4425
  765. theorem OAI.DeligneDrinfeld.WordGrading.mem_space_iff line 4435
  766. theorem OAI.DeligneDrinfeld.WordGrading.mul_mem line 4443
  767. def OAI.DeligneDrinfeld.WordGrading.project line 4457
  768. theorem OAI.DeligneDrinfeld.WordGrading.project_word line 4460
  769. theorem OAI.DeligneDrinfeld.WordGrading.project_coeff line 4463
  770. theorem OAI.DeligneDrinfeld.WordGrading.project_mem line 4481
  771. theorem OAI.DeligneDrinfeld.WordGrading.project_eq_self line 4486
  772. theorem OAI.DeligneDrinfeld.WordGrading.project_eq_zero line 4493
  773. def OAI.DeligneDrinfeld.WordGrading.degree line 4501
  774. theorem OAI.DeligneDrinfeld.WordGrading.degree_one line 4502
  775. theorem OAI.DeligneDrinfeld.WordGrading.degree_of line 4503
  776. theorem OAI.DeligneDrinfeld.WordGrading.degree_mul line 4504
  777. def OAI.DeligneDrinfeld.WordGrading.homogeneous line 4506
  778. def OAI.DeligneDrinfeld.WordGrading.above line 4507
  779. def OAI.DeligneDrinfeld.WordGrading.below line 4508
  780. def OAI.DeligneDrinfeld.WordGrading.piece line 4509
  781. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_mul line 4510
  782. theorem OAI.DeligneDrinfeld.WordGrading.above_mul line 4513
  783. theorem OAI.DeligneDrinfeld.WordGrading.below_mul line 4516
  784. theorem OAI.DeligneDrinfeld.WordGrading.map_space line 4519
  785. theorem OAI.DeligneDrinfeld.WordGrading.deriv_homogeneous line 4528
  786. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_above line 4544
  787. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_below line 4546
  788. theorem OAI.DeligneDrinfeld.WordGrading.deriv_above line 4549
  789. theorem OAI.DeligneDrinfeld.WordGrading.deriv_below line 4567
  790. theorem OAI.DeligneDrinfeld.WordGrading.deriv_sub line 4585
  791. def OAI.DeligneDrinfeld.TriangularWords.action line 4601
  792. theorem OAI.DeligneDrinfeld.TriangularWords.action_atom line 4602
  793. def OAI.DeligneDrinfeld.TriangularWords.apply line 4604
  794. theorem OAI.DeligneDrinfeld.TriangularWords.apply_word_one line 4606
  795. theorem OAI.DeligneDrinfeld.TriangularWords.apply_word_cons line 4607
  796. theorem OAI.DeligneDrinfeld.TriangularWords.comparison line 4611
  797. def OAI.DeligneDrinfeld.WordGrading.strictlyBelow line 4639
  798. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_mul_strictlyBelow line 4640
  799. theorem OAI.DeligneDrinfeld.WordGrading.strictlyBelow_mul_homogeneous line 4643
  800. theorem OAI.DeligneDrinfeld.WordGrading.deriv_strictlyBelow line 4647
  801. abbrev OAI.DeligneDrinfeld.TensorGrading.V line 4667
  802. def OAI.DeligneDrinfeld.TensorGrading.space line 4668
  803. theorem OAI.DeligneDrinfeld.TensorGrading.tmul_word_mem line 4670
  804. theorem OAI.DeligneDrinfeld.TensorGrading.space_mono line 4673
  805. theorem OAI.DeligneDrinfeld.TensorGrading.tmul_mem line 4678
  806. def OAI.DeligneDrinfeld.TensorGrading.homogeneous line 4694
  807. def OAI.DeligneDrinfeld.TensorGrading.above line 4696
  808. def OAI.DeligneDrinfeld.TensorGrading.below line 4698
  809. def OAI.DeligneDrinfeld.TensorGrading.strictlyBelow line 4700
  810. theorem OAI.DeligneDrinfeld.TensorGrading.map_space line 4703
  811. theorem OAI.DeligneDrinfeld.TensorGrading.homo_tmul line 4712
  812. theorem OAI.DeligneDrinfeld.TensorGrading.above_tmul line 4715
  813. theorem OAI.DeligneDrinfeld.TensorGrading.below_tmul line 4718
  814. theorem OAI.DeligneDrinfeld.TensorGrading.strict_homo_tmul line 4721
  815. theorem OAI.DeligneDrinfeld.TensorGrading.op_homogeneous line 4726
  816. theorem OAI.DeligneDrinfeld.TensorGrading.op_above line 4748
  817. theorem OAI.DeligneDrinfeld.TensorGrading.op_below line 4774
  818. theorem OAI.DeligneDrinfeld.TensorGrading.op_strictlyBelow line 4800
  819. theorem OAI.DeligneDrinfeld.TensorGrading.op_difference line 4813
  820. theorem OAI.DeligneDrinfeld.TensorGrading.op_difference_above line 4823
  821. theorem OAI.DeligneDrinfeld.TensorGrading.op_difference_below line 4839
  822. theorem OAI.DeligneDrinfeld.TensorGrading.comparison_above line 4855
  823. theorem OAI.DeligneDrinfeld.TensorGrading.comparison_below line 4868
  824. abbrev OAI.DeligneDrinfeld.CountTables.K line 4885
  825. abbrev OAI.DeligneDrinfeld.CountTables.F line 4886
  826. abbrev OAI.DeligneDrinfeld.CountTables.B line 4887
  827. def OAI.DeligneDrinfeld.CountTables.H line 4889
  828. def OAI.DeligneDrinfeld.CountTables.U line 4890
  829. def OAI.DeligneDrinfeld.CountTables.V line 4891
  830. def OAI.DeligneDrinfeld.CountTables.bracket line 4892
  831. def OAI.DeligneDrinfeld.CountTables.R' line 4893
  832. def OAI.DeligneDrinfeld.CountTables.Q line 4894
  833. def OAI.DeligneDrinfeld.CountTables.W line 4895
  834. def OAI.DeligneDrinfeld.CountTables.common line 4896
  835. def OAI.DeligneDrinfeld.CountTables.higher line 4909
  836. def OAI.DeligneDrinfeld.CountTables.lower line 4920
  837. def OAI.DeligneDrinfeld.CountTables.source line 4923
  838. def OAI.DeligneDrinfeld.CountTables.target line 4924
  839. def OAI.DeligneDrinfeld.CountTables.fiberCount line 4926
  840. def OAI.DeligneDrinfeld.CountTables.baseCount line 4927
  841. theorem OAI.DeligneDrinfeld.CountTables.bracket_homo line 4931
  842. theorem OAI.DeligneDrinfeld.CountTables.H_homo line 4937
  843. theorem OAI.DeligneDrinfeld.CountTables.U_homo line 4938
  844. theorem OAI.DeligneDrinfeld.CountTables.V_homo line 4941
  845. theorem OAI.DeligneDrinfeld.CountTables.R_homo line 4944
  846. theorem OAI.DeligneDrinfeld.CountTables.Q_homo line 4947
  847. theorem OAI.DeligneDrinfeld.CountTables.W_homo line 4951
  848. theorem OAI.DeligneDrinfeld.CountTables.common_homo_0 line 4957
  849. theorem OAI.DeligneDrinfeld.CountTables.common_homo_1 line 4967
  850. theorem OAI.DeligneDrinfeld.CountTables.common_homo_2 line 4977
  851. theorem OAI.DeligneDrinfeld.CountTables.common_homo_3 line 4988
  852. theorem OAI.DeligneDrinfeld.CountTables.common_homo line 4999
  853. theorem OAI.DeligneDrinfeld.CountTables.higher_homo_0 line 5005
  854. theorem OAI.DeligneDrinfeld.CountTables.higher_homo_1 line 5015
  855. theorem OAI.DeligneDrinfeld.CountTables.higher_homo_2 line 5025
  856. theorem OAI.DeligneDrinfeld.CountTables.higher_homo_3 line 5032
  857. theorem OAI.DeligneDrinfeld.CountTables.higher_homo line 5044
  858. theorem OAI.DeligneDrinfeld.CountTables.lower_strict line 5051
  859. theorem OAI.DeligneDrinfeld.CountTables.source_above line 5058
  860. theorem OAI.DeligneDrinfeld.CountTables.source_difference line 5065
  861. theorem OAI.DeligneDrinfeld.CountTables.target_below line 5071
  862. theorem OAI.DeligneDrinfeld.CountTables.target_difference line 5078
  863. theorem OAI.DeligneDrinfeld.CountTables.source_comparison line 5083
  864. theorem OAI.DeligneDrinfeld.CountTables.target_comparison line 5089
  865. abbrev OAI.DeligneDrinfeld.CountTables.G line 5097
  866. def OAI.DeligneDrinfeld.CountTables.X line 5098
  867. def OAI.DeligneDrinfeld.CountTables.Y line 5099
  868. def OAI.DeligneDrinfeld.CountTables.C line 5100
  869. def OAI.DeligneDrinfeld.CountTables.realize line 5101
  870. def OAI.DeligneDrinfeld.CountTables.δ line 5103
  871. def OAI.DeligneDrinfeld.CountTables.ε line 5104
  872. def OAI.DeligneDrinfeld.CountTables.baseDeriv line 5105
  873. theorem OAI.DeligneDrinfeld.CountTables.realize_H line 5111
  874. theorem OAI.DeligneDrinfeld.CountTables.realize_U line 5112
  875. theorem OAI.DeligneDrinfeld.CountTables.realize_V line 5113
  876. theorem OAI.DeligneDrinfeld.CountTables.realize_bracket line 5114
  877. theorem OAI.DeligneDrinfeld.CountTables.deriv_bracket line 5115
  878. theorem OAI.DeligneDrinfeld.CountTables.bracket_add_left line 5119
  879. theorem OAI.DeligneDrinfeld.CountTables.bracket_add_right line 5120
  880. theorem OAI.DeligneDrinfeld.CountTables.bracket_sub_left line 5121
  881. theorem OAI.DeligneDrinfeld.CountTables.bracket_sub_right line 5122
  882. theorem OAI.DeligneDrinfeld.CountTables.bracket_zero_left line 5123
  883. theorem OAI.DeligneDrinfeld.CountTables.bracket_zero_right line 5124
  884. theorem OAI.DeligneDrinfeld.CountTables.bracket_self line 5125
  885. theorem OAI.DeligneDrinfeld.CountTables.bracket_swap line 5126
  886. theorem OAI.DeligneDrinfeld.CountTables.bracket_ad_square line 5127
  887. theorem OAI.DeligneDrinfeld.CountTables.bracket_leibniz line 5132
  888. theorem OAI.DeligneDrinfeld.CountTables.δ_X line 5134
  889. theorem OAI.DeligneDrinfeld.CountTables.δ_Y_self line 5135
  890. theorem OAI.DeligneDrinfeld.CountTables.δ_Y_other line 5136
  891. theorem OAI.DeligneDrinfeld.CountTables.δ_mul line 5139
  892. theorem OAI.DeligneDrinfeld.CountTables.δ_bracket line 5140
  893. theorem OAI.DeligneDrinfeld.CountTables.δ_H line 5141
  894. theorem OAI.DeligneDrinfeld.CountTables.bracket_X_Y line 5145
  895. theorem OAI.DeligneDrinfeld.CountTables.bracket_X_C line 5146
  896. theorem OAI.DeligneDrinfeld.CountTables.δ_C_self line 5147
  897. theorem OAI.DeligneDrinfeld.CountTables.δ_C_other line 5151
  898. theorem OAI.DeligneDrinfeld.CountTables.ε_X line 5153
  899. theorem OAI.DeligneDrinfeld.CountTables.ε_Y line 5154
  900. theorem OAI.DeligneDrinfeld.CountTables.ε_bracket line 5155
  901. theorem OAI.DeligneDrinfeld.CountTables.ε_H line 5156
  902. theorem OAI.DeligneDrinfeld.CountTables.ε_C line 5157
  903. def OAI.DeligneDrinfeld.CountTables.J line 5161
  904. theorem OAI.DeligneDrinfeld.CountTables.J_X line 5162
  905. theorem OAI.DeligneDrinfeld.CountTables.J_Y_zero line 5165
  906. theorem OAI.DeligneDrinfeld.CountTables.J_Y_one line 5169
  907. theorem OAI.DeligneDrinfeld.CountTables.J_bracket line 5173
  908. theorem OAI.DeligneDrinfeld.CountTables.J_mul line 5177
  909. theorem OAI.DeligneDrinfeld.CountTables.J_H line 5181
  910. theorem OAI.DeligneDrinfeld.CountTables.J_C_zero line 5188
  911. theorem OAI.DeligneDrinfeld.CountTables.J_C_one line 5193
  912. theorem OAI.DeligneDrinfeld.CountTables.δ_square_H line 5199
  913. theorem OAI.DeligneDrinfeld.CountTables.δ_H_add_C line 5203
  914. theorem OAI.DeligneDrinfeld.CountTables.δ_square_C_self line 5205
  915. theorem OAI.DeligneDrinfeld.CountTables.δ_square_C_other line 5209
  916. theorem OAI.DeligneDrinfeld.CountTables.realize_atom_zero line 5213
  917. theorem OAI.DeligneDrinfeld.CountTables.realize_atom_one line 5214
  918. theorem OAI.DeligneDrinfeld.CountTables.realize_atom_two line 5215
  919. theorem OAI.DeligneDrinfeld.CountTables.realize_atom_three line 5216
  920. theorem OAI.DeligneDrinfeld.CountTables.realize_atom_four line 5217
  921. theorem OAI.DeligneDrinfeld.CountTables.source_realization_a0 line 5220
  922. theorem OAI.DeligneDrinfeld.CountTables.source_realization_a1 line 5224
  923. theorem OAI.DeligneDrinfeld.CountTables.source_realization_u line 5228
  924. theorem OAI.DeligneDrinfeld.CountTables.source_realization_v line 5230
  925. theorem OAI.DeligneDrinfeld.CountTables.source_realization line 5236
  926. def OAI.DeligneDrinfeld.WeightedDeletion.raw line 5246
  927. def OAI.DeligneDrinfeld.WeightedDeletion.op line 5250
  928. theorem OAI.DeligneDrinfeld.WeightedDeletion.op_word line 5253
  929. inductive OAI.DeligneDrinfeld.WeightedDeletion.Step line 5256
  930. theorem OAI.DeligneDrinfeld.WeightedDeletion.raw_mem_space line 5260
  931. theorem OAI.DeligneDrinfeld.WeightedDeletion.Step.length line 5280
  932. theorem OAI.DeligneDrinfeld.WeightedDeletion.raw_length line 5286
  933. def OAI.DeligneDrinfeld.WeightedDeletion.count line 5290
  934. theorem OAI.DeligneDrinfeld.WeightedDeletion.count_nil line 5291
  935. theorem OAI.DeligneDrinfeld.WeightedDeletion.count_cons line 5292
  936. theorem OAI.DeligneDrinfeld.WeightedDeletion.Step.count_bound line 5294
  937. theorem OAI.DeligneDrinfeld.WeightedDeletion.raw_count_bound line 5301