OAI/Algebra/Drinfeld/BraidExp.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RealDeligneDrinfeld.FreeCutoffCategory.P line 11
  2. abbrev OAI.RealDeligneDrinfeld.FreeCutoffCategory.Q line 12
  3. abbrev OAI.RealDeligneDrinfeld.FreeCutoffCategory.F line 13
  4. def OAI.RealDeligneDrinfeld.FreeCutoffCategory.j line 15
  5. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.j_of line 16
  6. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.j_mem line 19
  7. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.lie_mem line 22
  8. def OAI.RealDeligneDrinfeld.FreeCutoffCategory.velocity line 26
  9. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.velocity_mem line 27
  10. def OAI.RealDeligneDrinfeld.FreeCutoffCategory.d line 35
  11. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.d_one line 38
  12. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.d_mul line 40
  13. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.d_mem line 43
  14. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.d_j line 45
  15. def OAI.RealDeligneDrinfeld.FreeCutoffCategory.h line 50
  16. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.h_mem line 51
  17. def OAI.RealDeligneDrinfeld.FreeCutoffCategory.data line 60
  18. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.loop_j line 63
  19. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.unit_all line 69
  20. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.raises line 75
  21. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.nilpotent line 80
  22. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.unit line 85
  23. theorem OAI.RealDeligneDrinfeld.FreeCutoffCategory.leading line 90
  24. def OAI.RealDeligneDrinfeld.BraidCutoff.presentation line 104
  25. abbrev OAI.RealDeligneDrinfeld.BraidCutoff.Q line 106
  26. abbrev OAI.RealDeligneDrinfeld.BraidCutoff.F line 107
  27. def OAI.RealDeligneDrinfeld.BraidCutoff.freeMap line 109
  28. theorem OAI.RealDeligneDrinfeld.BraidCutoff.freeMap_relation line 112
  29. def OAI.RealDeligneDrinfeld.BraidCutoff.lieMap line 115
  30. def OAI.RealDeligneDrinfeld.BraidCutoff.projection line 127
  31. theorem OAI.RealDeligneDrinfeld.BraidCutoff.lieMap_projection line 131
  32. theorem OAI.RealDeligneDrinfeld.BraidCutoff.projection_of line 132
  33. theorem OAI.RealDeligneDrinfeld.BraidCutoff.lieMap_of line 134
  34. theorem OAI.RealDeligneDrinfeld.BraidCutoff.projection_relation line 140
  35. theorem OAI.RealDeligneDrinfeld.BraidCutoff.lie_mem line 143
  36. theorem OAI.RealDeligneDrinfeld.BraidCutoff.t_mem line 146
  37. theorem OAI.RealDeligneDrinfeld.BraidCutoff.weight_mem line 157
  38. theorem OAI.RealDeligneDrinfeld.BraidCutoff.eval_mem line 172
  39. theorem OAI.RealDeligneDrinfeld.BraidCutoff.A_mem line 179
  40. theorem OAI.RealDeligneDrinfeld.BraidCutoff.D_mem line 181
  41. theorem OAI.RealDeligneDrinfeld.BraidCutoff.E_mem line 183
  42. def OAI.RealDeligneDrinfeld.BraidCutoff.velocity line 186
  43. theorem OAI.RealDeligneDrinfeld.BraidCutoff.velocity_mem line 189
  44. theorem OAI.RealDeligneDrinfeld.BraidCutoff.relations_killed line 222
  45. def OAI.RealDeligneDrinfeld.BraidCutoff.derivation line 230
  46. theorem OAI.RealDeligneDrinfeld.BraidCutoff.derivation_lieMap line 234
  47. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.B_mem line 247
  48. def OAI.RealDeligneDrinfeld.BraidCategoryExp.h line 251
  49. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.h_mem line 253
  50. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.d_one line 264
  51. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.d_mul line 266
  52. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.d_mem line 269
  53. def OAI.RealDeligneDrinfeld.BraidCategoryExp.data line 273
  54. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.raises line 276
  55. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.nilpotent line 281
  56. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.loop_lieMap line 286
  57. theorem OAI.RealDeligneDrinfeld.BraidCategoryExp.unit line 297
  58. def OAI.RealDeligneDrinfeld.BraidInsertionExp.family line 310
  59. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.family_mem line 312
  60. def OAI.RealDeligneDrinfeld.BraidInsertionExp.insert line 314
  61. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.insert_gen line 316
  62. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.insert_j line 318
  63. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.edge line 329
  64. abbrev OAI.RealDeligneDrinfeld.BraidInsertionExp.IAB line 342
  65. abbrev OAI.RealDeligneDrinfeld.BraidInsertionExp.IAD line 343
  66. abbrev OAI.RealDeligneDrinfeld.BraidInsertionExp.IDE line 344
  67. abbrev OAI.RealDeligneDrinfeld.BraidInsertionExp.IBC line 345
  68. abbrev OAI.RealDeligneDrinfeld.BraidInsertionExp.ICE line 347
  69. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.pentagon_preserved line 350
  70. def OAI.DeligneDrinfeld.CategoryExp.sum line 373
  71. theorem OAI.DeligneDrinfeld.CategoryExp.sum_apply line 382
  72. theorem OAI.DeligneDrinfeld.CategoryExp.sum_raises line 384
  73. theorem OAI.DeligneDrinfeld.CategoryExp.sum_nilpotent line 391
  74. theorem OAI.DeligneDrinfeld.CategoryExp.sum_natural line 396
  75. theorem OAI.DeligneDrinfeld.CategoryExp.exp_sum_natural line 402
  76. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.edge_derivative line 418
  77. def OAI.RealDeligneDrinfeld.BraidInsertionSum.free line 435
  78. def OAI.RealDeligneDrinfeld.BraidInsertionSum.braid line 436
  79. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.free_raises line 438
  80. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.braid_raises line 444
  81. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.free_nilpotent line 451
  82. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.braid_nilpotent line 453
  83. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.edge line 455
  84. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.pentagon line 467
  85. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.unit line 483
  86. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.edge_formula line 486
  87. theorem OAI.DeligneDrinfeld.CategoryExp.pow_difference line 506
  88. theorem OAI.DeligneDrinfeld.CategoryExp.exp_difference line 520
  89. theorem OAI.DeligneDrinfeld.CategoryExp.exp_difference_unit line 547