OAI/Algebra/Drinfeld/Pentagon.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.FourFrames.corner_reverse line 15
  2. theorem OAI.DeligneDrinfeld.FourFrames.DE_insertion line 22
  3. theorem OAI.DeligneDrinfeld.FourFrames.CE_insertion line 30
  4. theorem OAI.DeligneDrinfeld.FourFrames.associator_pentagon line 37
  5. def OAI.RealDeligneDrinfeld.KZBraidPentagon.F line 61
  6. def OAI.RealDeligneDrinfeld.KZBraidPentagon.generic line 69
  7. theorem OAI.RealDeligneDrinfeld.KZBraidPentagon.generic_t line 82
  8. theorem OAI.RealDeligneDrinfeld.KZBraidPentagon.chords_mem line 84
  9. theorem OAI.RealDeligneDrinfeld.KZBraidPentagon.insert_associator line 87
  10. theorem OAI.RealDeligneDrinfeld.KZBraidPentagon.pentagon line 95
  11. theorem OAI.RealDeligneDrinfeld.KZBraidPentagon.positive line 109
  12. theorem OAI.RealDeligneDrinfeld.KZBraidPentagon.negative line 112
  13. def OAI.DeligneDrinfeld.EulerPBW.affine line 121
  14. theorem OAI.DeligneDrinfeld.EulerPBW.affine_apply line 131
  15. def OAI.DeligneDrinfeld.EulerPBW.affineHom line 134
  16. def OAI.DeligneDrinfeld.EulerPBW.dynkin line 166
  17. theorem OAI.DeligneDrinfeld.EulerPBW.dynkin_iota line 170
  18. theorem OAI.DeligneDrinfeld.EulerPBW.injective_iota line 177
  19. abbrev OAI.DeligneDrinfeld.LieCutoffFaithful.S line 189
  20. def OAI.DeligneDrinfeld.LieCutoffFaithful.z line 191
  21. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.z_pow line 193
  22. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.z_pow_zero line 197
  23. def OAI.DeligneDrinfeld.LieCutoffFaithful.lift line 210
  24. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.lift_atom line 213
  25. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.lift_word line 217
  26. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.lift_above line 226
  27. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.lift_weight line 234
  28. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.lift_piece line 249
  29. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.coefficient_z_pow line 259
  30. def OAI.DeligneDrinfeld.LieCutoffFaithful.extract line 269
  31. theorem OAI.DeligneDrinfeld.LieCutoffFaithful.extract_tmul line 273
  32. def OAI.RealDeligneDrinfeld.AffineWeight.op line 284
  33. theorem OAI.RealDeligneDrinfeld.AffineWeight.op_lie line 294
  34. def OAI.RealDeligneDrinfeld.AffineWeight.homogeneous line 306
  35. theorem OAI.RealDeligneDrinfeld.AffineWeight.homogeneous_lie line 324
  36. def OAI.RealDeligneDrinfeld.AffineWeight.representation line 330
  37. theorem OAI.RealDeligneDrinfeld.AffineWeight.word_rep line 333
  38. theorem OAI.RealDeligneDrinfeld.AffineWeight.weight_rep line 340
  39. theorem OAI.RealDeligneDrinfeld.AffineWeight.homogeneous_injective line 349
  40. abbrev OAI.RealDeligneDrinfeld.BraidCutoff.Piece line 363
  41. theorem OAI.RealDeligneDrinfeld.BraidCutoff.of_mem line 364
  42. theorem OAI.RealDeligneDrinfeld.BraidCutoff.chord_mem line 366
  43. theorem OAI.RealDeligneDrinfeld.BraidCutoff.piece_lie line 372
  44. theorem OAI.RealDeligneDrinfeld.BraidCutoff.relation_piece line 383
  45. def OAI.RealDeligneDrinfeld.BraidCutoff.affineGenerators line 388
  46. theorem OAI.RealDeligneDrinfeld.BraidCutoff.projection_eq line 389
  47. theorem OAI.RealDeligneDrinfeld.BraidCutoff.affine_weight line 393
  48. def OAI.RealDeligneDrinfeld.BraidCutoff.representation line 399
  49. theorem OAI.RealDeligneDrinfeld.BraidCutoff.representation_quotient line 407
  50. theorem OAI.RealDeligneDrinfeld.BraidCutoff.detect line 411
  51. theorem OAI.DeligneDrinfeld.TopDifference.product_zero line 426
  52. theorem OAI.DeligneDrinfeld.TopDifference.reverse_zero line 429
  53. theorem OAI.DeligneDrinfeld.TopDifference.product line 432
  54. theorem OAI.DeligneDrinfeld.TopDifference.normalized_product line 442
  55. theorem OAI.DeligneDrinfeld.TopDifference.triple line 451
  56. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.insert_mem line 464
  57. theorem OAI.RealDeligneDrinfeld.BraidInsertionExp.linear_pentagon_difference line 467
  58. def OAI.RealDeligneDrinfeld.PentagonDetect.value line 499
  59. theorem OAI.RealDeligneDrinfeld.PentagonDetect.eval_mem line 503
  60. theorem OAI.RealDeligneDrinfeld.PentagonDetect.homogeneous line 510
  61. theorem OAI.RealDeligneDrinfeld.PentagonDetect.projection_chord line 517
  62. theorem OAI.RealDeligneDrinfeld.PentagonDetect.projection_eval line 518
  63. theorem OAI.RealDeligneDrinfeld.PentagonDetect.detect line 524
  64. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.value_sum line 540
  65. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.residual_top line 545
  66. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.coefficient_solution line 548