OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical304.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9728 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw9728step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw9728step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9728 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw9729 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw9729step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw9729step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9729 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw9730 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw9730step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw9730step1 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw9730step2 line 66
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9730 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw9731 line 86
  15. def OAI.MUB6.Certificate.PairSemantics.raw9731step0 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw9731step1 line 90
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical9731 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw9732 line 106
  19. def OAI.MUB6.Certificate.PairSemantics.raw9732step0 line 108
  20. def OAI.MUB6.Certificate.PairSemantics.raw9732step1 line 110
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9732 line 112
  22. def OAI.MUB6.Certificate.PairSemantics.raw9733 line 126
  23. def OAI.MUB6.Certificate.PairSemantics.raw9733step0 line 128
  24. def OAI.MUB6.Certificate.PairSemantics.raw9733step1 line 130
  25. def OAI.MUB6.Certificate.PairSemantics.raw9733step2 line 132
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9733 line 134
  27. def OAI.MUB6.Certificate.PairSemantics.raw9734 line 152
  28. def OAI.MUB6.Certificate.PairSemantics.raw9734step0 line 154
  29. def OAI.MUB6.Certificate.PairSemantics.raw9734step1 line 156
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9734 line 158
  31. def OAI.MUB6.Certificate.PairSemantics.raw9735 line 172
  32. def OAI.MUB6.Certificate.PairSemantics.raw9735step0 line 174
  33. def OAI.MUB6.Certificate.PairSemantics.raw9735step1 line 176
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9735 line 178
  35. def OAI.MUB6.Certificate.PairSemantics.raw9736 line 191
  36. def OAI.MUB6.Certificate.PairSemantics.raw9736step0 line 193
  37. def OAI.MUB6.Certificate.PairSemantics.raw9736step1 line 195
  38. def OAI.MUB6.Certificate.PairSemantics.raw9736step2 line 197
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9736 line 199
  40. def OAI.MUB6.Certificate.PairSemantics.raw9737 line 216
  41. def OAI.MUB6.Certificate.PairSemantics.raw9737step0 line 218
  42. def OAI.MUB6.Certificate.PairSemantics.raw9737step1 line 220
  43. def OAI.MUB6.Certificate.PairSemantics.raw9737step2 line 222
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9737 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw9738 line 241
  46. def OAI.MUB6.Certificate.PairSemantics.raw9738step0 line 243
  47. def OAI.MUB6.Certificate.PairSemantics.raw9738step1 line 245
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical9738 line 247
  49. def OAI.MUB6.Certificate.PairSemantics.raw9739 line 260
  50. def OAI.MUB6.Certificate.PairSemantics.raw9739step0 line 262
  51. def OAI.MUB6.Certificate.PairSemantics.raw9739step1 line 264
  52. def OAI.MUB6.Certificate.PairSemantics.raw9739step2 line 266
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9739 line 268
  54. def OAI.MUB6.Certificate.PairSemantics.raw9740 line 285
  55. def OAI.MUB6.Certificate.PairSemantics.raw9740step0 line 287
  56. def OAI.MUB6.Certificate.PairSemantics.raw9740step1 line 289
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9740 line 291
  58. def OAI.MUB6.Certificate.PairSemantics.raw9741 line 304
  59. def OAI.MUB6.Certificate.PairSemantics.raw9741step0 line 306
  60. def OAI.MUB6.Certificate.PairSemantics.raw9741step1 line 308
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9741 line 310
  62. def OAI.MUB6.Certificate.PairSemantics.raw9742 line 323
  63. def OAI.MUB6.Certificate.PairSemantics.raw9742step0 line 325
  64. def OAI.MUB6.Certificate.PairSemantics.raw9742step1 line 327
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9742 line 329
  66. def OAI.MUB6.Certificate.PairSemantics.raw9743 line 342
  67. def OAI.MUB6.Certificate.PairSemantics.raw9743step0 line 344
  68. def OAI.MUB6.Certificate.PairSemantics.raw9743step1 line 346
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9743 line 348
  70. def OAI.MUB6.Certificate.PairSemantics.raw9744 line 361
  71. def OAI.MUB6.Certificate.PairSemantics.raw9744step0 line 363
  72. def OAI.MUB6.Certificate.PairSemantics.raw9744step1 line 365
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical9744 line 367
  74. def OAI.MUB6.Certificate.PairSemantics.raw9745 line 380
  75. def OAI.MUB6.Certificate.PairSemantics.raw9745step0 line 382
  76. def OAI.MUB6.Certificate.PairSemantics.raw9745step1 line 384
  77. def OAI.MUB6.Certificate.PairSemantics.raw9745step2 line 386
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9745 line 388
  79. def OAI.MUB6.Certificate.PairSemantics.raw9746 line 405
  80. def OAI.MUB6.Certificate.PairSemantics.raw9746step0 line 407
  81. def OAI.MUB6.Certificate.PairSemantics.raw9746step1 line 409
  82. def OAI.MUB6.Certificate.PairSemantics.raw9746step2 line 411
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9746 line 413
  84. def OAI.MUB6.Certificate.PairSemantics.raw9747 line 430
  85. def OAI.MUB6.Certificate.PairSemantics.raw9747step0 line 432
  86. def OAI.MUB6.Certificate.PairSemantics.raw9747step1 line 434
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9747 line 436
  88. def OAI.MUB6.Certificate.PairSemantics.raw9748 line 449
  89. def OAI.MUB6.Certificate.PairSemantics.raw9748step0 line 451
  90. def OAI.MUB6.Certificate.PairSemantics.raw9748step1 line 453
  91. def OAI.MUB6.Certificate.PairSemantics.raw9748step2 line 455
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9748 line 457
  93. def OAI.MUB6.Certificate.PairSemantics.raw9749 line 474
  94. def OAI.MUB6.Certificate.PairSemantics.raw9749step0 line 476
  95. def OAI.MUB6.Certificate.PairSemantics.raw9749step1 line 478
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9749 line 480
  97. def OAI.MUB6.Certificate.PairSemantics.raw9750 line 493
  98. def OAI.MUB6.Certificate.PairSemantics.raw9750step0 line 495
  99. def OAI.MUB6.Certificate.PairSemantics.raw9750step1 line 497
  100. def OAI.MUB6.Certificate.PairSemantics.raw9750step2 line 499
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical9750 line 501
  102. def OAI.MUB6.Certificate.PairSemantics.raw9751 line 518
  103. def OAI.MUB6.Certificate.PairSemantics.raw9751step0 line 520
  104. def OAI.MUB6.Certificate.PairSemantics.raw9751step1 line 522
  105. def OAI.MUB6.Certificate.PairSemantics.raw9751step2 line 524
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical9751 line 526
  107. def OAI.MUB6.Certificate.PairSemantics.raw9752 line 543
  108. def OAI.MUB6.Certificate.PairSemantics.raw9752step0 line 545
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical9752 line 547
  110. def OAI.MUB6.Certificate.PairSemantics.raw9753 line 556
  111. def OAI.MUB6.Certificate.PairSemantics.raw9753step0 line 558
  112. def OAI.MUB6.Certificate.PairSemantics.raw9753step1 line 560
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical9753 line 562
  114. def OAI.MUB6.Certificate.PairSemantics.raw9754 line 575
  115. def OAI.MUB6.Certificate.PairSemantics.raw9754step0 line 577
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical9754 line 579
  117. def OAI.MUB6.Certificate.PairSemantics.raw9755 line 588
  118. def OAI.MUB6.Certificate.PairSemantics.raw9755step0 line 590
  119. def OAI.MUB6.Certificate.PairSemantics.raw9755step1 line 592
  120. def OAI.MUB6.Certificate.PairSemantics.raw9755step2 line 594
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical9755 line 596
  122. def OAI.MUB6.Certificate.PairSemantics.raw9756 line 613
  123. def OAI.MUB6.Certificate.PairSemantics.raw9756step0 line 615
  124. def OAI.MUB6.Certificate.PairSemantics.raw9756step1 line 617
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical9756 line 619
  126. def OAI.MUB6.Certificate.PairSemantics.raw9757 line 632
  127. def OAI.MUB6.Certificate.PairSemantics.raw9757step0 line 634
  128. def OAI.MUB6.Certificate.PairSemantics.raw9757step1 line 636
  129. def OAI.MUB6.Certificate.PairSemantics.raw9757step2 line 638
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical9757 line 640
  131. def OAI.MUB6.Certificate.PairSemantics.raw9758 line 657
  132. def OAI.MUB6.Certificate.PairSemantics.raw9758step0 line 659
  133. def OAI.MUB6.Certificate.PairSemantics.raw9758step1 line 661
  134. theorem OAI.MUB6.Certificate.PairSemantics.canonical9758 line 663
  135. def OAI.MUB6.Certificate.PairSemantics.raw9759 line 676
  136. def OAI.MUB6.Certificate.PairSemantics.raw9759step0 line 678
  137. def OAI.MUB6.Certificate.PairSemantics.raw9759step1 line 680
  138. def OAI.MUB6.Certificate.PairSemantics.raw9759step2 line 682
  139. theorem OAI.MUB6.Certificate.PairSemantics.canonical9759 line 684