OAI/Algebra/Drinfeld/RealBraid.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RealDeligneDrinfeld.BraidSix.total line 10
  2. def OAI.RealDeligneDrinfeld.BraidSix.matrix line 12
  3. structure OAI.RealDeligneDrinfeld.BraidSix.Relations line 15
  4. theorem OAI.RealDeligneDrinfeld.BraidSix.bf line 26
  5. theorem OAI.RealDeligneDrinfeld.BraidSix.dK line 33
  6. theorem OAI.RealDeligneDrinfeld.BraidSix.eL line 38
  7. theorem OAI.RealDeligneDrinfeld.BraidSix.aM line 43
  8. theorem OAI.RealDeligneDrinfeld.BraidSix.eM line 49
  9. theorem OAI.RealDeligneDrinfeld.BraidSix.fM line 57
  10. theorem OAI.RealDeligneDrinfeld.BraidSix.dP line 62
  11. theorem OAI.RealDeligneDrinfeld.BraidSix.cP line 68
  12. theorem OAI.RealDeligneDrinfeld.BraidSix.fP line 76
  13. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_self line 81
  14. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_symm line 84
  15. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_disjoint_0 line 87
  16. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_disjoint_1 line 99
  17. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_disjoint_2 line 111
  18. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_disjoint_3 line 123
  19. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_disjoint line 135
  20. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_three_0 line 144
  21. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_three_1 line 162
  22. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_three_2 line 180
  23. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_three_3 line 198
  24. theorem OAI.RealDeligneDrinfeld.BraidSix.matrix_three line 216
  25. def OAI.RealDeligneDrinfeld.T4Basic.a line 230
  26. def OAI.RealDeligneDrinfeld.T4Basic.b line 231
  27. def OAI.RealDeligneDrinfeld.T4Basic.c line 232
  28. def OAI.RealDeligneDrinfeld.T4Basic.d line 233
  29. def OAI.RealDeligneDrinfeld.T4Basic.e line 234
  30. def OAI.RealDeligneDrinfeld.T4Basic.f line 235
  31. theorem OAI.RealDeligneDrinfeld.T4Basic.induction line 237
  32. theorem OAI.RealDeligneDrinfeld.T4Basic.hom_ext line 252
  33. theorem OAI.RealDeligneDrinfeld.T4Basic.matrix_t line 263
  34. theorem OAI.RealDeligneDrinfeld.T4Basic.central_a line 266
  35. theorem OAI.RealDeligneDrinfeld.T4Basic.central_b line 276
  36. theorem OAI.RealDeligneDrinfeld.T4Basic.central_c line 286
  37. theorem OAI.RealDeligneDrinfeld.T4Basic.central_d line 296
  38. theorem OAI.RealDeligneDrinfeld.T4Basic.central_e line 306
  39. theorem OAI.RealDeligneDrinfeld.T4Basic.central_f line 316
  40. theorem OAI.RealDeligneDrinfeld.T4Basic.central line 326
  41. theorem OAI.RealDeligneDrinfeld.T4Basic.relations line 342
  42. structure OAI.RealDeligneDrinfeld.TangentBraid.Data line 368
  43. theorem OAI.RealDeligneDrinfeld.TangentBraid.crossing line 386
  44. theorem OAI.RealDeligneDrinfeld.TangentBraid.inner_pair line 396
  45. theorem OAI.RealDeligneDrinfeld.TangentBraid.commute_lie line 401
  46. def OAI.RealDeligneDrinfeld.TangentBraid.va line 404
  47. def OAI.RealDeligneDrinfeld.TangentBraid.vb line 405
  48. def OAI.RealDeligneDrinfeld.TangentBraid.vc line 406
  49. def OAI.RealDeligneDrinfeld.TangentBraid.vd line 407
  50. def OAI.RealDeligneDrinfeld.TangentBraid.ve line 408
  51. def OAI.RealDeligneDrinfeld.TangentBraid.vf line 409
  52. theorem OAI.RealDeligneDrinfeld.TangentBraid.vd_tangent line 411
  53. theorem OAI.RealDeligneDrinfeld.TangentBraid.bC line 414
  54. theorem OAI.RealDeligneDrinfeld.TangentBraid.ve_tangent line 420
  55. theorem OAI.RealDeligneDrinfeld.TangentBraid.gauge_difference line 427
  56. theorem OAI.RealDeligneDrinfeld.TangentBraid.crossing_de line 432
  57. theorem OAI.RealDeligneDrinfeld.TangentBraid.velocity_K line 437
  58. theorem OAI.RealDeligneDrinfeld.TangentBraid.velocity_L line 438
  59. theorem OAI.RealDeligneDrinfeld.TangentBraid.velocity_b line 444
  60. theorem OAI.RealDeligneDrinfeld.TangentBraid.velocity_c line 446
  61. theorem OAI.RealDeligneDrinfeld.TangentBraid.velocity_total line 451
  62. def OAI.RealDeligneDrinfeld.TangentBraid.ja line 456
  63. def OAI.RealDeligneDrinfeld.TangentBraid.jb line 457
  64. def OAI.RealDeligneDrinfeld.TangentBraid.jc line 458
  65. def OAI.RealDeligneDrinfeld.TangentBraid.jd line 459
  66. def OAI.RealDeligneDrinfeld.TangentBraid.je line 460
  67. def OAI.RealDeligneDrinfeld.TangentBraid.jf line 461
  68. theorem OAI.RealDeligneDrinfeld.TangentBraid.relations line 463
  69. theorem OAI.RealDeligneDrinfeld.TriangleSolutions.third line 513
  70. theorem OAI.RealDeligneDrinfeld.TriangleSolutions.shift_u line 519
  71. theorem OAI.RealDeligneDrinfeld.TriangleSolutions.shift_v line 526
  72. theorem OAI.RealDeligneDrinfeld.TriangleSolutions.cyclic line 533
  73. theorem OAI.RealDeligneDrinfeld.TriangleSolutions.special line 540
  74. def OAI.RealDeligneDrinfeld.T4SolutionData.A line 558
  75. def OAI.RealDeligneDrinfeld.T4SolutionData.B line 559
  76. def OAI.RealDeligneDrinfeld.T4SolutionData.C line 560
  77. def OAI.RealDeligneDrinfeld.T4SolutionData.D line 561
  78. def OAI.RealDeligneDrinfeld.T4SolutionData.E line 562
  79. def OAI.RealDeligneDrinfeld.T4SolutionData.H line 563
  80. def OAI.RealDeligneDrinfeld.T4SolutionData.I line 564
  81. def OAI.RealDeligneDrinfeld.T4SolutionData.J line 565
  82. def OAI.RealDeligneDrinfeld.T4SolutionData.P line 566
  83. def OAI.RealDeligneDrinfeld.T4SolutionData.Q line 567
  84. theorem OAI.RealDeligneDrinfeld.T4SolutionData.pentagon line 569
  85. theorem OAI.RealDeligneDrinfeld.T4SolutionData.permuted line 575
  86. theorem OAI.RealDeligneDrinfeld.T4SolutionData.data line 585
  87. def OAI.RealDeligneDrinfeld.T4Derivation.jets line 616
  88. theorem OAI.RealDeligneDrinfeld.T4Derivation.jets_base line 620
  89. def OAI.RealDeligneDrinfeld.T4Derivation.lift line 624
  90. theorem OAI.RealDeligneDrinfeld.T4Derivation.lift_t line 630
  91. theorem OAI.RealDeligneDrinfeld.T4Derivation.lift_base line 633
  92. def OAI.RealDeligneDrinfeld.T4Derivation.derivation line 642
  93. theorem OAI.RealDeligneDrinfeld.T4Derivation.derivation_t line 650
  94. theorem OAI.RealDeligneDrinfeld.T4Derivation.derivation_a line 655
  95. theorem OAI.RealDeligneDrinfeld.T4Derivation.derivation_b line 657
  96. theorem OAI.RealDeligneDrinfeld.T4Derivation.derivation_c line 659
  97. theorem OAI.RealDeligneDrinfeld.T4Derivation.derivation_d line 661
  98. theorem OAI.RealDeligneDrinfeld.T4Derivation.derivation_e line 663
  99. theorem OAI.RealDeligneDrinfeld.T4Derivation.derivation_f line 666
  100. theorem OAI.RealDeligneDrinfeld.GaugeCompatibility.intertwine line 675
  101. theorem OAI.RealDeligneDrinfeld.GaugeCompatibility.compatible line 691
  102. def OAI.RealDeligneDrinfeld.ThreeSolutionCategory.data line 710
  103. theorem OAI.RealDeligneDrinfeld.ThreeSolutionCategory.loop_zero line 713
  104. theorem OAI.RealDeligneDrinfeld.ThreeSolutionCategory.value line 716
  105. theorem OAI.RealDeligneDrinfeld.ThreeSolutionCategory.anti line 718
  106. theorem OAI.RealDeligneDrinfeld.ThreeSolutionCategory.rotating_anti line 721
  107. theorem OAI.RealDeligneDrinfeld.ThreeSolutionCategory.rotating_twice line 730
  108. theorem OAI.RealDeligneDrinfeld.ThreeSolutionCategory.swap line 737
  109. theorem OAI.RealDeligneDrinfeld.ThreeSolutionCategory.rotate line 756
  110. def OAI.RealDeligneDrinfeld.FourSolutionCategory.data line 788
  111. theorem OAI.RealDeligneDrinfeld.FourSolutionCategory.edge line 791
  112. theorem OAI.RealDeligneDrinfeld.FourSolutionCategory.AB line 802
  113. theorem OAI.RealDeligneDrinfeld.FourSolutionCategory.AD line 809
  114. theorem OAI.RealDeligneDrinfeld.FourSolutionCategory.DE line 817
  115. theorem OAI.RealDeligneDrinfeld.FourSolutionCategory.BC line 831
  116. theorem OAI.RealDeligneDrinfeld.FourSolutionCategory.CE line 855
  117. def OAI.RealDeligneDrinfeld.CategoricalValues.ofSolution line 879
  118. theorem OAI.RealDeligneDrinfeld.CategoricalValues.value_ofSolution line 895