OAI/Algebra/Drinfeld/Reduction.lean

GitHub source file

353 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.AlphabetTransport.renameAssoc_atom line 12
  2. theorem OAI.DeligneDrinfeld.AlphabetTransport.assoc_comp line 15
  3. theorem OAI.DeligneDrinfeld.AlphabetTransport.assoc_retract line 21
  4. theorem OAI.DeligneDrinfeld.AlphabetTransport.assoc_injective line 29
  5. abbrev OAI.DeligneDrinfeld.QuadraticLeading.K line 38
  6. def OAI.DeligneDrinfeld.QuadraticLeading.bitOption line 41
  7. def OAI.DeligneDrinfeld.QuadraticLeading.letters line 47
  8. def OAI.DeligneDrinfeld.QuadraticLeading.under line 53
  9. theorem OAI.DeligneDrinfeld.QuadraticLeading.under_apply line 55
  10. theorem OAI.DeligneDrinfeld.QuadraticLeading.quad_transport line 57
  11. theorem OAI.DeligneDrinfeld.QuadraticLeading.quad_transport_inv line 64
  12. theorem OAI.DeligneDrinfeld.QuadraticLeading.quad_injective line 71
  13. theorem OAI.DeligneDrinfeld.QuadraticLeading.under_injective line 78
  14. theorem OAI.DeligneDrinfeld.QuadraticLeading.degree_length line 82
  15. theorem OAI.DeligneDrinfeld.QuadraticLeading.tree_degree_length line 85
  16. theorem OAI.DeligneDrinfeld.QuadraticLeading.representation line 89
  17. theorem OAI.DeligneDrinfeld.QuadraticLeading.quad_homogeneous line 117
  18. theorem OAI.DeligneDrinfeld.QuadraticLeading.representation_weight line 132
  19. theorem OAI.DeligneDrinfeld.QuadraticLeading.weight_count line 140
  20. theorem OAI.DeligneDrinfeld.QuadraticLeading.leading_ac line 147
  21. theorem OAI.DeligneDrinfeld.QuadraticLeading.leading_rows line 156
  22. theorem OAI.DeligneDrinfeld.QuadraticLeading.leading_no_C line 166
  23. def OAI.DeligneDrinfeld.BaseChangeEquations.special line 186
  24. theorem OAI.DeligneDrinfeld.BaseChangeEquations.cast_special line 189
  25. theorem OAI.DeligneDrinfeld.BaseChangeEquations.reduce_special line 193
  26. theorem OAI.DeligneDrinfeld.BaseChangeEquations.eval_comp line 203
  27. theorem OAI.DeligneDrinfeld.BaseChangeEquations.eval_self line 206
  28. theorem OAI.DeligneDrinfeld.BaseChangeEquations.swapped line 213
  29. theorem OAI.DeligneDrinfeld.TwoModule.add_self line 221
  30. theorem OAI.DeligneDrinfeld.TwoModule.neg_eq line 225
  31. theorem OAI.DeligneDrinfeld.TwoModule.sub_eq_add line 229
  32. theorem OAI.DeligneDrinfeld.TwoModule.eq_of_add_zero line 231
  33. abbrev OAI.DeligneDrinfeld.BaseChangeEquations.K line 236
  34. theorem OAI.DeligneDrinfeld.BaseChangeEquations.deletion_special line 238
  35. def OAI.DeligneDrinfeld.WordGrading.lower line 253
  36. theorem OAI.DeligneDrinfeld.WordGrading.lower_mul_homogeneous line 255
  37. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_mul_lower line 259
  38. theorem OAI.DeligneDrinfeld.WordGrading.deriv_lower line 263
  39. theorem OAI.DeligneDrinfeld.WordGrading.deriv_lowers_above line 277
  40. theorem OAI.DeligneDrinfeld.WordGrading.lower_homogeneous line 287
  41. theorem OAI.DeligneDrinfeld.WordGrading.piece_zero_of_above line 291
  42. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_add_high_zero line 295
  43. abbrev OAI.DeligneDrinfeld.ResidualKernel.K line 307
  44. def OAI.DeligneDrinfeld.ResidualKernel.low line 310
  45. def OAI.DeligneDrinfeld.ResidualKernel.high line 311
  46. def OAI.DeligneDrinfeld.ResidualKernel.delta line 312
  47. def OAI.DeligneDrinfeld.ResidualKernel.tau line 314
  48. def OAI.DeligneDrinfeld.ResidualKernel.tau0 line 316
  49. theorem OAI.DeligneDrinfeld.ResidualKernel.deriv_add line 319
  50. theorem OAI.DeligneDrinfeld.ResidualKernel.delta_split line 323
  51. theorem OAI.DeligneDrinfeld.ResidualKernel.quad_delta line 325
  52. theorem OAI.DeligneDrinfeld.ResidualKernel.quad_tau line 347
  53. theorem OAI.DeligneDrinfeld.ResidualKernel.embed_eval line 358
  54. theorem OAI.DeligneDrinfeld.ResidualKernel.full_equation line 363
  55. theorem OAI.DeligneDrinfeld.ResidualKernel.low_degree line 378
  56. theorem OAI.DeligneDrinfeld.ResidualKernel.high_degree line 384
  57. theorem OAI.DeligneDrinfeld.ResidualKernel.tau0_degree line 395
  58. theorem OAI.DeligneDrinfeld.ResidualKernel.tau_difference line 401
  59. theorem OAI.DeligneDrinfeld.ResidualKernel.tau_degree line 412
  60. theorem OAI.DeligneDrinfeld.ResidualKernel.leading_equation line 420
  61. def OAI.DeligneDrinfeld.ResidualKernel.coeff line 457
  62. def OAI.DeligneDrinfeld.ResidualKernel.monomial line 458
  63. theorem OAI.DeligneDrinfeld.ResidualKernel.monomial_nil line 460
  64. theorem OAI.DeligneDrinfeld.ResidualKernel.monomial_cons line 461
  65. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_add line 463
  66. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_smul line 464
  67. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_zero line 465
  68. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_monomial line 466
  69. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_monomial_fun line 471
  70. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_one_nil line 474
  71. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_one_cons line 475
  72. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_atom_mul_nil line 478
  73. theorem OAI.DeligneDrinfeld.ResidualKernel.coeff_atom_mul_cons line 484
  74. def OAI.DeligneDrinfeld.ResidualKernel.collapse line 499
  75. def OAI.DeligneDrinfeld.ResidualKernel.fills line 501
  76. def OAI.DeligneDrinfeld.ResidualKernel.noC line 505
  77. theorem OAI.DeligneDrinfeld.ResidualKernel.noC_nil line 507
  78. theorem OAI.DeligneDrinfeld.ResidualKernel.noC_cons line 508
  79. theorem OAI.DeligneDrinfeld.ResidualKernel.noC_append line 509
  80. theorem OAI.DeligneDrinfeld.ResidualKernel.tau0_atom line 511
  81. theorem OAI.DeligneDrinfeld.ResidualKernel.tau0_monomial_coeff line 514
  82. theorem OAI.DeligneDrinfeld.ResidualKernel.deriv_tau0_monomial_coeff line 531
  83. theorem OAI.DeligneDrinfeld.ResidualKernel.deriv_tau0_coeff line 556
  84. theorem OAI.DeligneDrinfeld.ResidualKernel.collapse_eq line 573
  85. theorem OAI.DeligneDrinfeld.ResidualKernel.collapse_noC line 574
  86. theorem OAI.DeligneDrinfeld.ResidualKernel.fills_noC line 581
  87. theorem OAI.DeligneDrinfeld.ResidualKernel.fills_prefix line 588
  88. theorem OAI.DeligneDrinfeld.ResidualKernel.fills_two line 595
  89. theorem OAI.DeligneDrinfeld.ResidualKernel.fills_three line 600
  90. def OAI.DeligneDrinfeld.ResidualKernel.count line 606
  91. theorem OAI.DeligneDrinfeld.ResidualKernel.count_nil line 607
  92. theorem OAI.DeligneDrinfeld.ResidualKernel.count_cons line 608
  93. theorem OAI.DeligneDrinfeld.ResidualKernel.count_append line 609
  94. theorem OAI.DeligneDrinfeld.ResidualKernel.noC_count line 612
  95. theorem OAI.DeligneDrinfeld.ResidualKernel.low_c_degree line 619
  96. theorem OAI.DeligneDrinfeld.ResidualKernel.low_noC_coeff line 625
  97. theorem OAI.DeligneDrinfeld.ResidualKernel.fills_sum_zero line 636
  98. theorem OAI.DeligneDrinfeld.ResidualKernel.adjacent_exchange line 643
  99. theorem OAI.DeligneDrinfeld.ResidualKernel.noC_perm line 652
  100. theorem OAI.DeligneDrinfeld.ResidualKernel.coefficient_perm line 655
  101. theorem OAI.DeligneDrinfeld.ResidualKernel.count_list line 676
  102. theorem OAI.DeligneDrinfeld.ResidualKernel.count_replicate line 683
  103. theorem OAI.DeligneDrinfeld.ResidualKernel.perm_of_counts line 688
  104. theorem OAI.DeligneDrinfeld.ResidualKernel.coefficient_eq_counts line 698
  105. theorem OAI.DeligneDrinfeld.ResidualKernel.triple_zero line 703
  106. theorem OAI.DeligneDrinfeld.ResidualKernel.coefficient_zero_two_As line 718
  107. theorem OAI.DeligneDrinfeld.ResidualKernel.residual_zero line 732
  108. theorem OAI.DeligneDrinfeld.ResidualKernel.lie_palindrome_zero line 747
  109. theorem OAI.DeligneDrinfeld.LetterRetraction.support_of_mem line 781
  110. theorem OAI.DeligneDrinfeld.LetterRetraction.single_letter line 803
  111. theorem OAI.DeligneDrinfeld.LetterRetraction.homogeneous_single_zero line 823
  112. abbrev OAI.DeligneDrinfeld.ProjectionKernel.K line 845
  113. theorem OAI.DeligneDrinfeld.ProjectionKernel.degree_congr_word line 847
  114. theorem OAI.DeligneDrinfeld.ProjectionKernel.degree_scale line 853
  115. theorem OAI.DeligneDrinfeld.ProjectionKernel.ac_zero line 859
  116. theorem OAI.DeligneDrinfeld.ProjectionKernel.b_zero line 868
  117. theorem OAI.DeligneDrinfeld.ProjectionKernel.a_from_ac_noC line 873
  118. theorem OAI.DeligneDrinfeld.ProjectionKernel.higher_single_B line 880
  119. def OAI.DeligneDrinfeld.ProjectionKernel.yWeight line 895
  120. def OAI.DeligneDrinfeld.ProjectionKernel.xSlot line 896
  121. def OAI.DeligneDrinfeld.ProjectionKernel.ySlot line 897
  122. def OAI.DeligneDrinfeld.ProjectionKernel.swap line 899
  123. theorem OAI.DeligneDrinfeld.ProjectionKernel.swap_atom line 901
  124. theorem OAI.DeligneDrinfeld.ProjectionKernel.quad_y line 904
  125. theorem OAI.DeligneDrinfeld.ProjectionKernel.swap_quad_y line 919
  126. theorem OAI.DeligneDrinfeld.ProjectionKernel.symmetry_r_two line 934
  127. theorem OAI.DeligneDrinfeld.ProjectionKernel.one_A_two_B_zero line 974
  128. theorem OAI.DeligneDrinfeld.ProjectionKernel.leading_projection_kernel line 1000
  129. theorem OAI.DeligneDrinfeld.WordGrading.above_reflect line 1073
  130. def OAI.DeligneDrinfeld.EliminationGraded.collapse line 1088
  131. theorem OAI.DeligneDrinfeld.EliminationGraded.collapse_atom line 1091
  132. theorem OAI.DeligneDrinfeld.EliminationGraded.collapse_embed line 1094
  133. theorem OAI.DeligneDrinfeld.EliminationGraded.operator_collapse line 1102
  134. theorem OAI.DeligneDrinfeld.EliminationGraded.extract_collapse line 1110
  135. theorem OAI.DeligneDrinfeld.EliminationGraded.collapse_injective line 1114
  136. theorem OAI.DeligneDrinfeld.EliminationGraded.adWord_degree line 1117
  137. theorem OAI.DeligneDrinfeld.EliminationGraded.embed_decompose line 1136
  138. theorem OAI.DeligneDrinfeld.EliminationGraded.trace_homogeneous_zero line 1143
  139. abbrev OAI.DeligneDrinfeld.OreShift.S line 1174
  140. def OAI.DeligneDrinfeld.OreShift.C line 1176
  141. def OAI.DeligneDrinfeld.OreShift.B line 1177
  142. def OAI.DeligneDrinfeld.OreShift.wt line 1178
  143. def OAI.DeligneDrinfeld.OreShift.D line 1180
  144. theorem OAI.DeligneDrinfeld.OreShift.D_C line 1181
  145. theorem OAI.DeligneDrinfeld.OreShift.D_B line 1182
  146. theorem OAI.DeligneDrinfeld.OreShift.D_one line 1183
  147. theorem OAI.DeligneDrinfeld.OreShift.D_mul line 1184
  148. theorem OAI.DeligneDrinfeld.OreShift.D_lie line 1185
  149. theorem OAI.DeligneDrinfeld.OreShift.D_square line 1187
  150. theorem OAI.DeligneDrinfeld.OreShift.above_zero line 1197
  151. theorem OAI.DeligneDrinfeld.OreShift.above_lie line 1199
  152. def OAI.DeligneDrinfeld.OreShift.P line 1204
  153. theorem OAI.DeligneDrinfeld.OreShift.P_zero line 1208
  154. theorem OAI.DeligneDrinfeld.OreShift.P_succ line 1209
  155. theorem OAI.DeligneDrinfeld.OreShift.D_F line 1213
  156. theorem OAI.DeligneDrinfeld.OreShift.P_one line 1215
  157. theorem OAI.DeligneDrinfeld.OreShift.P_above line 1220
  158. theorem OAI.DeligneDrinfeld.OreShift.DP_one line 1232
  159. theorem OAI.DeligneDrinfeld.OreShift.DP_above line 1234
  160. theorem OAI.DeligneDrinfeld.OreShift.D_lie_square line 1246
  161. theorem OAI.DeligneDrinfeld.OreShift.DP_even line 1258
  162. def OAI.DeligneDrinfeld.OreShift.indexWt line 1277
  163. def OAI.DeligneDrinfeld.OreShift.factor line 1279
  164. def OAI.DeligneDrinfeld.OreShift.operators line 1283
  165. def OAI.DeligneDrinfeld.OreShift.constant line 1284
  166. theorem OAI.DeligneDrinfeld.OreShift.constant_one line 1287
  167. theorem OAI.DeligneDrinfeld.OreShift.constant_atom_mul line 1288
  168. theorem OAI.DeligneDrinfeld.OreShift.factor_bounds line 1293
  169. theorem OAI.DeligneDrinfeld.OreShift.word_bound line 1307
  170. theorem OAI.DeligneDrinfeld.OreShift.constant_bound line 1337
  171. abbrev OAI.DeligneDrinfeld.EvenIndex.K line 1351
  172. theorem OAI.DeligneDrinfeld.EvenIndex.map_lie line 1353
  173. def OAI.DeligneDrinfeld.EvenIndex.abc line 1356
  174. def OAI.DeligneDrinfeld.EvenIndex.idx line 1362
  175. def OAI.DeligneDrinfeld.EvenIndex.unidx line 1363
  176. theorem OAI.DeligneDrinfeld.EvenIndex.idx_left line 1365
  177. def OAI.DeligneDrinfeld.EvenIndex.intoABC line 1371
  178. theorem OAI.DeligneDrinfeld.EvenIndex.intoABC_injective line 1374
  179. theorem OAI.DeligneDrinfeld.EvenIndex.intoABC_atom line 1378
  180. def OAI.DeligneDrinfeld.EvenIndex.evenWt line 1382
  181. theorem OAI.DeligneDrinfeld.EvenIndex.intoABC_degree line 1384
  182. def OAI.DeligneDrinfeld.EvenIndex.input line 1402
  183. theorem OAI.DeligneDrinfeld.EvenIndex.input_atom line 1405
  184. theorem OAI.DeligneDrinfeld.EvenIndex.intoABC_atom_zero line 1409
  185. theorem OAI.DeligneDrinfeld.EvenIndex.intoABC_atom_one line 1411
  186. theorem OAI.DeligneDrinfeld.EvenIndex.intoABC_atom_two line 1413
  187. theorem OAI.DeligneDrinfeld.EvenIndex.input_atom_zero line 1422
  188. theorem OAI.DeligneDrinfeld.EvenIndex.input_atom_succ line 1424
  189. theorem OAI.DeligneDrinfeld.EvenIndex.quad_intoABC line 1429
  190. def OAI.DeligneDrinfeld.EvenIndex.fiber line 1448
  191. theorem OAI.DeligneDrinfeld.EvenIndex.input_fiber line 1451
  192. theorem OAI.DeligneDrinfeld.EvenIndex.intoABC_fiber line 1466
  193. theorem OAI.DeligneDrinfeld.EvenIndex.termwise_bound line 1475
  194. def OAI.DeligneDrinfeld.EvenIndex.xWeight line 1488
  195. def OAI.DeligneDrinfeld.EvenIndex.swappedInput line 1489
  196. theorem OAI.DeligneDrinfeld.EvenIndex.swappedInput_degree line 1491
  197. theorem OAI.DeligneDrinfeld.EvenIndex.quad_x line 1508
  198. theorem OAI.DeligneDrinfeld.EvenIndex.swapped_solution line 1523
  199. theorem OAI.DeligneDrinfeld.EvenIndex.selected_expression line 1529
  200. def OAI.DeligneDrinfeld.OreShift.evaluate line 1554
  201. theorem OAI.DeligneDrinfeld.OreShift.evaluate_x line 1557
  202. theorem OAI.DeligneDrinfeld.OreShift.evaluate_y line 1558
  203. def OAI.DeligneDrinfeld.OreShift.eraseShift line 1560
  204. theorem OAI.DeligneDrinfeld.OreShift.comm_D_left line 1563
  205. theorem OAI.DeligneDrinfeld.OreShift.left_comm_D line 1569
  206. theorem OAI.DeligneDrinfeld.OreShift.evaluate_quad line 1573
  207. theorem OAI.DeligneDrinfeld.OreShift.evaluate_lie line 1590
  208. theorem OAI.DeligneDrinfeld.OreShift.evaluate_swapped line 1594
  209. theorem OAI.DeligneDrinfeld.OreShift.eraseShift_retract line 1623
  210. theorem OAI.DeligneDrinfeld.OreShift.eraseShift_word line 1629
  211. theorem OAI.DeligneDrinfeld.OreShift.erase_selector line 1634
  212. def OAI.DeligneDrinfeld.OreShift.translate line 1655
  213. theorem OAI.DeligneDrinfeld.OreShift.translate_C line 1657
  214. theorem OAI.DeligneDrinfeld.OreShift.translate_B line 1658
  215. theorem OAI.DeligneDrinfeld.OreShift.translate_erase line 1660
  216. theorem OAI.DeligneDrinfeld.OreShift.selected_constant line 1665
  217. theorem OAI.DeligneDrinfeld.OreShift.shifted_leading_bound line 1674
  218. def OAI.DeligneDrinfeld.PositionalDeletion.replaceWord line 1693
  219. def OAI.DeligneDrinfeld.PositionalDeletion.replace line 1699
  220. theorem OAI.DeligneDrinfeld.PositionalDeletion.replace_word line 1703
  221. theorem OAI.DeligneDrinfeld.PositionalDeletion.replace_one line 1707
  222. theorem OAI.DeligneDrinfeld.PositionalDeletion.replace_C_mul line 1712
  223. theorem OAI.DeligneDrinfeld.PositionalDeletion.replace_B_mul_zero line 1722
  224. theorem OAI.DeligneDrinfeld.PositionalDeletion.replace_B_mul_succ line 1731
  225. def OAI.DeligneDrinfeld.PositionalDeletion.countB line 1741
  226. theorem OAI.DeligneDrinfeld.PositionalDeletion.countB_nil line 1743
  227. theorem OAI.DeligneDrinfeld.PositionalDeletion.countB_false line 1744
  228. theorem OAI.DeligneDrinfeld.PositionalDeletion.countB_true line 1745
  229. theorem OAI.DeligneDrinfeld.PositionalDeletion.replaceWord_missing line 1747
  230. theorem OAI.DeligneDrinfeld.PositionalDeletion.word_cons line 1761
  231. theorem OAI.DeligneDrinfeld.PositionalDeletion.replaceWord_append line 1765
  232. abbrev OAI.DeligneDrinfeld.GapWord.G line 1790
  233. def OAI.DeligneDrinfeld.GapWord.prepend line 1792
  234. def OAI.DeligneDrinfeld.GapWord.bump line 1793
  235. def OAI.DeligneDrinfeld.GapWord.encode line 1795
  236. def OAI.DeligneDrinfeld.GapWord.decode line 1799
  237. theorem OAI.DeligneDrinfeld.GapWord.decode_false_prefix line 1804
  238. theorem OAI.DeligneDrinfeld.GapWord.decode_encode line 1810
  239. theorem OAI.DeligneDrinfeld.GapWord.encode_bump line 1816
  240. theorem OAI.DeligneDrinfeld.GapWord.encode_prepend line 1821
  241. theorem OAI.DeligneDrinfeld.GapWord.encode_decode line 1826
  242. def OAI.DeligneDrinfeld.GapWord.size line 1832
  243. theorem OAI.DeligneDrinfeld.GapWord.size_bump line 1834
  244. theorem OAI.DeligneDrinfeld.GapWord.size_prepend line 1835
  245. theorem OAI.DeligneDrinfeld.GapWord.size_decode line 1837
  246. def OAI.DeligneDrinfeld.GapWord.merge line 1843
  247. def OAI.DeligneDrinfeld.GapWord.erase line 1848
  248. theorem OAI.DeligneDrinfeld.GapWord.erase_small line 1853
  249. theorem OAI.DeligneDrinfeld.GapWord.erase_merge line 1866
  250. def OAI.DeligneDrinfeld.GapAlgebra.alg line 1919
  251. def OAI.DeligneDrinfeld.GapAlgebra.optionAlg line 1920
  252. theorem OAI.DeligneDrinfeld.GapAlgebra.optionAlg_none line 1922
  253. theorem OAI.DeligneDrinfeld.GapAlgebra.optionAlg_some line 1923
  254. theorem OAI.DeligneDrinfeld.GapAlgebra.word_false_pow line 1925
  255. theorem OAI.DeligneDrinfeld.GapAlgebra.alg_bump line 1930
  256. theorem OAI.DeligneDrinfeld.GapAlgebra.alg_prepend line 1936
  257. theorem OAI.DeligneDrinfeld.GapAlgebra.optionAlg_prepend line 1942
  258. theorem OAI.DeligneDrinfeld.GapAlgebra.alg_nil line 1948
  259. theorem OAI.DeligneDrinfeld.GapAlgebra.alg_cons line 1951
  260. theorem OAI.DeligneDrinfeld.GapAlgebra.replace_C_pow_mul line 1954
  261. theorem OAI.DeligneDrinfeld.GapAlgebra.replace_alg line 1964
  262. def OAI.DeligneDrinfeld.GapAlgebra.eraseLinear line 1985
  263. theorem OAI.DeligneDrinfeld.GapAlgebra.eraseLinear_word line 1989
  264. theorem OAI.DeligneDrinfeld.GapAlgebra.eraseLinear_alg line 1993
  265. theorem OAI.DeligneDrinfeld.GapAlgebra.eraseLinear_optionAlg line 1997
  266. theorem OAI.DeligneDrinfeld.GapAlgebra.eraseLinear_replace_alg line 2003
  267. theorem OAI.DeligneDrinfeld.GapAlgebra.eraseLinear_replace_word line 2010
  268. theorem OAI.DeligneDrinfeld.WordGrading.algHom_difference_lower line 2023
  269. theorem OAI.DeligneDrinfeld.WordGrading.above_lower_zero line 2046
  270. theorem OAI.DeligneDrinfeld.OreShift.translate_difference line 2066
  271. theorem OAI.DeligneDrinfeld.OreShift.erase_degree line 2093
  272. theorem OAI.DeligneDrinfeld.OreShift.shift_invariant line 2099
  273. def OAI.DeligneDrinfeld.OreShift.shiftDeriv line 2119
  274. theorem OAI.DeligneDrinfeld.OreShift.shiftDeriv_C line 2121
  275. theorem OAI.DeligneDrinfeld.OreShift.shiftDeriv_B line 2122
  276. theorem OAI.DeligneDrinfeld.OreShift.shiftDeriv_one line 2123
  277. theorem OAI.DeligneDrinfeld.OreShift.shiftDeriv_mul line 2124
  278. theorem OAI.DeligneDrinfeld.OreShift.shiftDeriv_degree line 2127
  279. theorem OAI.DeligneDrinfeld.OreShift.taylor_remainder line 2135
  280. theorem OAI.DeligneDrinfeld.OreShift.shiftDeriv_zero line 2175
  281. theorem OAI.DeligneDrinfeld.PositionalDeletion.degree_countB line 2198
  282. theorem OAI.DeligneDrinfeld.PositionalDeletion.replace_mul line 2205
  283. theorem OAI.DeligneDrinfeld.PositionalDeletion.shiftDeriv_word line 2224
  284. theorem OAI.DeligneDrinfeld.PositionalDeletion.shiftDeriv_eq_sum line 2242
  285. theorem OAI.DeligneDrinfeld.WordGrading.exists_below line 2259
  286. def OAI.DeligneDrinfeld.GapSelection.cwt line 2276
  287. theorem OAI.DeligneDrinfeld.GapSelection.degree_countC line 2278
  288. theorem OAI.DeligneDrinfeld.GapSelection.eraseLinear_replace line 2285
  289. theorem OAI.DeligneDrinfeld.GapSelection.replace_missing_homogeneous line 2295
  290. theorem OAI.DeligneDrinfeld.GapSelection.Cpow_degree line 2306
  291. theorem OAI.DeligneDrinfeld.GapSelection.all_deletions_zero line 2316
  292. abbrev OAI.DeligneDrinfeld.GeneratorDeletion.K line 2336
  293. abbrev OAI.DeligneDrinfeld.GeneratorDeletion.I line 2337
  294. abbrev OAI.DeligneDrinfeld.GeneratorDeletion.Q line 2338
  295. def OAI.DeligneDrinfeld.GeneratorDeletion.removeWord line 2340
  296. def OAI.DeligneDrinfeld.GeneratorDeletion.remove line 2345
  297. theorem OAI.DeligneDrinfeld.GeneratorDeletion.remove_word line 2349
  298. def OAI.DeligneDrinfeld.GeneratorDeletion.zeroAt line 2353
  299. def OAI.DeligneDrinfeld.GeneratorDeletion.insertList line 2358
  300. def OAI.DeligneDrinfeld.GeneratorDeletion.insert line 2363
  301. theorem OAI.DeligneDrinfeld.GeneratorDeletion.insert_word line 2367
  302. theorem OAI.DeligneDrinfeld.GeneratorDeletion.insert_succ_atom_mul line 2371
  303. theorem OAI.DeligneDrinfeld.GeneratorDeletion.insert_remove_word line 2381
  304. theorem OAI.DeligneDrinfeld.GeneratorDeletion.insert_remove line 2404
  305. theorem OAI.DeligneDrinfeld.GeneratorDeletion.input_injective line 2413
  306. theorem OAI.DeligneDrinfeld.GeneratorDeletion.input_degree line 2416
  307. theorem OAI.DeligneDrinfeld.GeneratorDeletion.replace_input_atom_zero line 2428
  308. theorem OAI.DeligneDrinfeld.GeneratorDeletion.replace_input_word line 2440
  309. theorem OAI.DeligneDrinfeld.GeneratorDeletion.replace_input line 2459
  310. def OAI.DeligneDrinfeld.GeneratorDeletion.noZero line 2471
  311. theorem OAI.DeligneDrinfeld.GeneratorDeletion.noZero_of_zeroAt_false line 2473
  312. theorem OAI.DeligneDrinfeld.GeneratorDeletion.support_noZero line 2484
  313. def OAI.DeligneDrinfeld.GeneratorDeletion.retain line 2500
  314. theorem OAI.DeligneDrinfeld.GeneratorDeletion.retain_atom line 2502
  315. theorem OAI.DeligneDrinfeld.GeneratorDeletion.retain_word line 2504
  316. theorem OAI.DeligneDrinfeld.GeneratorDeletion.retain_eq_self line 2512
  317. def OAI.DeligneDrinfeld.GeneratorDeletion.cutLie line 2521
  318. def OAI.DeligneDrinfeld.GeneratorDeletion.includeLie line 2523
  319. def OAI.DeligneDrinfeld.GeneratorDeletion.cutAssoc line 2526
  320. def OAI.DeligneDrinfeld.GeneratorDeletion.includeAssoc line 2527
  321. theorem OAI.DeligneDrinfeld.GeneratorDeletion.cut_embed line 2529
  322. theorem OAI.DeligneDrinfeld.GeneratorDeletion.include_embed line 2537
  323. theorem OAI.DeligneDrinfeld.GeneratorDeletion.include_cut line 2544
  324. theorem OAI.DeligneDrinfeld.GeneratorDeletion.positive_generation line 2550
  325. abbrev OAI.DeligneDrinfeld.ImageBound.K line 2570
  326. theorem OAI.DeligneDrinfeld.ImageBound.input_fiber_of_bcount line 2572
  327. def OAI.DeligneDrinfeld.ImageBound.positiveInput line 2588
  328. theorem OAI.DeligneDrinfeld.ImageBound.positiveInput_injective line 2590
  329. theorem OAI.DeligneDrinfeld.ImageBound.positiveInput_atom line 2598
  330. theorem OAI.DeligneDrinfeld.ImageBound.shift_invariant_generation line 2601
  331. def OAI.DeligneDrinfeld.ImageBound.eraseLie line 2615
  332. theorem OAI.DeligneDrinfeld.ImageBound.erase_embed line 2619
  333. def OAI.DeligneDrinfeld.ImageBound.leading line 2626
  334. theorem OAI.DeligneDrinfeld.ImageBound.embed_leading line 2629
  335. theorem OAI.DeligneDrinfeld.ImageBound.leading_bcount line 2633
  336. def OAI.DeligneDrinfeld.ImageBound.cbWeight line 2638
  337. theorem OAI.DeligneDrinfeld.ImageBound.erase_weight_degree line 2640
  338. theorem OAI.DeligneDrinfeld.ImageBound.leading_weight line 2647
  339. theorem OAI.DeligneDrinfeld.ImageBound.weight_count line 2652
  340. theorem OAI.DeligneDrinfeld.ImageBound.weight_split line 2659
  341. theorem OAI.DeligneDrinfeld.ImageBound.D_Cpow line 2671
  342. theorem OAI.DeligneDrinfeld.ImageBound.C_lie_Cpow line 2676
  343. theorem OAI.DeligneDrinfeld.ImageBound.leading_shift_invariant line 2680
  344. theorem OAI.DeligneDrinfeld.ImageBound.actual_image_positive line 2691
  345. theorem OAI.DeligneDrinfeld.ImageBound.degree_bcount_zero line 2704
  346. theorem OAI.DeligneDrinfeld.ImageBound.leading_zero_count line 2717
  347. theorem OAI.DeligneDrinfeld.ImageBound.positiveInput_degree line 2722
  348. theorem OAI.DeligneDrinfeld.ImageBound.positiveInput_bcount line 2731
  349. def OAI.DeligneDrinfeld.ImageBound.oddWeight line 2734
  350. theorem OAI.DeligneDrinfeld.ImageBound.positiveInput_weight line 2736
  351. theorem OAI.DeligneDrinfeld.ImageBound.image_graded line 2739
  352. theorem OAI.DeligneDrinfeld.ImageBound.actual_image line 2749
  353. theorem OAI.DeligneDrinfeld.ImageBound.leading_D_zero line 2763