OAI/Algebra/Drinfeld/Grading.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.WordGrading.piece_homogeneous line 14
  2. theorem OAI.DeligneDrinfeld.WordGrading.piece_mem line 22
  3. theorem OAI.DeligneDrinfeld.WordGrading.piece_eq_self_iff line 25
  4. theorem OAI.DeligneDrinfeld.WordGrading.project_degree_homogeneous line 31
  5. theorem OAI.DeligneDrinfeld.WordGrading.algHom_project line 40
  6. theorem OAI.DeligneDrinfeld.WordGrading.algHom_piece line 53
  7. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_reflect line 57
  8. theorem OAI.DeligneDrinfeld.WordGrading.project_preserves line 64
  9. theorem OAI.DeligneDrinfeld.WordGrading.subtract_piece_above line 73
  10. def OAI.DeligneDrinfeld.LieGrading.treeDegree line 95
  11. theorem OAI.DeligneDrinfeld.LieGrading.treeDegree_leaf line 97
  12. theorem OAI.DeligneDrinfeld.LieGrading.treeDegree_node line 99
  13. theorem OAI.DeligneDrinfeld.LieGrading.embed_eval_homogeneous line 103
  14. def OAI.DeligneDrinfeld.LieGrading.homogeneousLie line 115
  15. theorem OAI.DeligneDrinfeld.LieGrading.piece_exists line 118
  16. def OAI.DeligneDrinfeld.LieGrading.piece line 137
  17. theorem OAI.DeligneDrinfeld.LieGrading.piece_spec line 140
  18. theorem OAI.DeligneDrinfeld.LieGrading.embed_piece line 144
  19. theorem OAI.DeligneDrinfeld.LieGrading.homogeneousLie_embed line 147
  20. theorem OAI.DeligneDrinfeld.LieGrading.homogeneous_iff line 157
  21. abbrev OAI.DeligneDrinfeld.TensorProjection.len line 177
  22. abbrev OAI.DeligneDrinfeld.TensorProjection.piece line 178
  23. def OAI.DeligneDrinfeld.TensorProjection.totalPiece line 180
  24. theorem OAI.DeligneDrinfeld.TensorProjection.totalPiece_word line 183
  25. theorem OAI.DeligneDrinfeld.TensorProjection.totalPiece_homogeneous line 207
  26. theorem OAI.DeligneDrinfeld.TensorProjection.homogeneous_mul line 219
  27. def OAI.DeligneDrinfeld.TensorProjection.coproduct line 243
  28. theorem OAI.DeligneDrinfeld.TensorProjection.coproduct_atom line 246
  29. theorem OAI.DeligneDrinfeld.TensorProjection.coproduct_word_homogeneous line 249
  30. theorem OAI.DeligneDrinfeld.TensorProjection.coproduct_piece line 262
  31. theorem OAI.DeligneDrinfeld.TensorProjection.totalPiece_left line 273
  32. theorem OAI.DeligneDrinfeld.TensorProjection.totalPiece_right line 287
  33. abbrev OAI.DeligneDrinfeld.PrimitiveWords.W line 303
  34. abbrev OAI.DeligneDrinfeld.PrimitiveWords.B line 304
  35. def OAI.DeligneDrinfeld.PrimitiveWords.word line 306
  36. def OAI.DeligneDrinfeld.PrimitiveWords.pair line 308
  37. def OAI.DeligneDrinfeld.PrimitiveWords.linear line 310
  38. def OAI.DeligneDrinfeld.PrimitiveWords.bilinear line 313
  39. theorem OAI.DeligneDrinfeld.PrimitiveWords.linear_single line 317
  40. theorem OAI.DeligneDrinfeld.PrimitiveWords.bilinear_single line 320
  41. theorem OAI.DeligneDrinfeld.PrimitiveWords.word_one line 324
  42. theorem OAI.DeligneDrinfeld.PrimitiveWords.word_mul line 325
  43. theorem OAI.DeligneDrinfeld.PrimitiveWords.pair_one line 327
  44. theorem OAI.DeligneDrinfeld.PrimitiveWords.pair_mul line 328
  45. def OAI.DeligneDrinfeld.PrimitiveWords.coproduct line 331
  46. def OAI.DeligneDrinfeld.PrimitiveWords.left line 334
  47. def OAI.DeligneDrinfeld.PrimitiveWords.right line 335
  48. def OAI.DeligneDrinfeld.PrimitiveWords.Primitive line 337
  49. def OAI.DeligneDrinfeld.PrimitiveWords.antipodeWord line 339
  50. def OAI.DeligneDrinfeld.PrimitiveWords.counitConvolution line 342
  51. def OAI.DeligneDrinfeld.PrimitiveWords.dynkinConvolution line 343
  52. theorem OAI.DeligneDrinfeld.PrimitiveWords.antipodeWord_one line 346
  53. theorem OAI.DeligneDrinfeld.PrimitiveWords.antipodeWord_cons line 347
  54. theorem OAI.DeligneDrinfeld.PrimitiveWords.coproduct_atom line 353
  55. theorem OAI.DeligneDrinfeld.PrimitiveWords.counitConvolution_left line 357
  56. theorem OAI.DeligneDrinfeld.PrimitiveWords.counitConvolution_right line 369
  57. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkinConvolution_left line 378
  58. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkinConvolution_right line 394
  59. theorem OAI.DeligneDrinfeld.PrimitiveWords.counitConvolution_one line 404
  60. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkinConvolution_one line 407
  61. theorem OAI.DeligneDrinfeld.PrimitiveWords.word_of line 411
  62. theorem OAI.DeligneDrinfeld.PrimitiveWords.counit_coproduct_word line 413
  63. def OAI.DeligneDrinfeld.PrimitiveWords.dynkinWord line 427
  64. def OAI.DeligneDrinfeld.PrimitiveWords.dynkin line 432
  65. def OAI.DeligneDrinfeld.PrimitiveWords.euler line 434
  66. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkin_coproduct_word line 436
  67. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkin_coproduct line 459
  68. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkin_left line 467
  69. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkin_right line 473
  70. theorem OAI.DeligneDrinfeld.PrimitiveWords.dynkin_primitive line 479
  71. theorem OAI.DeligneDrinfeld.PrimitiveWords.euler_homogeneous line 482
  72. theorem OAI.DeligneDrinfeld.PrimitiveWords.exists_lie_of_primitive line 493
  73. def OAI.DeligneDrinfeld.WordCoordinates.coordinates line 508
  74. theorem OAI.DeligneDrinfeld.WordCoordinates.coordinates_injective line 513
  75. def OAI.DeligneDrinfeld.WordCoordinates.assembly line 525
  76. theorem OAI.DeligneDrinfeld.WordCoordinates.coordinates_assembly line 528
  77. def OAI.DeligneDrinfeld.WordCoordinates.equiv line 534
  78. theorem OAI.DeligneDrinfeld.WordCoordinates.equiv_apply line 537
  79. instance OAI.DeligneDrinfeld.WordCoordinates.finite_space line 539
  80. theorem OAI.DeligneDrinfeld.WordCoordinates.length_le_degree line 544
  81. theorem OAI.DeligneDrinfeld.WordCoordinates.letter_le_degree line 554
  82. theorem OAI.DeligneDrinfeld.WordCoordinates.finite_degree line 564
  83. theorem OAI.DeligneDrinfeld.WordCoordinates.finite_degree_finite_alphabet line 576