OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical161.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5152 line 9
  2. def OAI.MUB6.Certificate.PairSemantics.raw5152step0 line 11
  3. def OAI.MUB6.Certificate.PairSemantics.raw5152step1 line 13
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5152 line 15
  5. def OAI.MUB6.Certificate.PairSemantics.raw5153 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw5153step0 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw5153step1 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5153 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw5154 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw5154step0 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw5154step1 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw5154step2 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical5154 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw5155 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw5155step0 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw5155step1 line 84
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5155 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw5156 line 102
  19. def OAI.MUB6.Certificate.PairSemantics.raw5156step0 line 104
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5156 line 106
  21. def OAI.MUB6.Certificate.PairSemantics.raw5157 line 117
  22. def OAI.MUB6.Certificate.PairSemantics.raw5157step0 line 119
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5157 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw5158 line 132
  25. def OAI.MUB6.Certificate.PairSemantics.raw5158step0 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw5158step1 line 136
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5158 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw5159 line 154
  29. def OAI.MUB6.Certificate.PairSemantics.raw5159step0 line 156
  30. def OAI.MUB6.Certificate.PairSemantics.raw5159step1 line 158
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5159 line 160
  32. def OAI.MUB6.Certificate.PairSemantics.raw5160 line 175
  33. def OAI.MUB6.Certificate.PairSemantics.raw5160step0 line 177
  34. def OAI.MUB6.Certificate.PairSemantics.raw5160step1 line 179
  35. def OAI.MUB6.Certificate.PairSemantics.raw5160step2 line 181
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5160 line 183
  37. def OAI.MUB6.Certificate.PairSemantics.raw5161 line 203
  38. def OAI.MUB6.Certificate.PairSemantics.raw5161step0 line 205
  39. def OAI.MUB6.Certificate.PairSemantics.raw5161step1 line 207
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5161 line 209
  41. def OAI.MUB6.Certificate.PairSemantics.raw5162 line 224
  42. def OAI.MUB6.Certificate.PairSemantics.raw5162step0 line 226
  43. def OAI.MUB6.Certificate.PairSemantics.raw5162step1 line 228
  44. def OAI.MUB6.Certificate.PairSemantics.raw5162step2 line 230
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5162 line 232
  46. def OAI.MUB6.Certificate.PairSemantics.raw5163 line 252
  47. def OAI.MUB6.Certificate.PairSemantics.raw5163step0 line 254
  48. def OAI.MUB6.Certificate.PairSemantics.raw5163step1 line 256
  49. def OAI.MUB6.Certificate.PairSemantics.raw5163step2 line 258
  50. def OAI.MUB6.Certificate.PairSemantics.raw5163step3 line 260
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5163 line 262
  52. def OAI.MUB6.Certificate.PairSemantics.raw5164 line 288
  53. def OAI.MUB6.Certificate.PairSemantics.raw5164step0 line 290
  54. def OAI.MUB6.Certificate.PairSemantics.raw5164step1 line 292
  55. def OAI.MUB6.Certificate.PairSemantics.raw5164step2 line 294
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5164 line 296
  57. def OAI.MUB6.Certificate.PairSemantics.raw5165 line 317
  58. def OAI.MUB6.Certificate.PairSemantics.raw5165step0 line 319
  59. def OAI.MUB6.Certificate.PairSemantics.raw5165step1 line 321
  60. def OAI.MUB6.Certificate.PairSemantics.raw5165step2 line 323
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5165 line 325
  62. def OAI.MUB6.Certificate.PairSemantics.raw5166 line 346
  63. def OAI.MUB6.Certificate.PairSemantics.raw5166step0 line 348
  64. def OAI.MUB6.Certificate.PairSemantics.raw5166step1 line 350
  65. def OAI.MUB6.Certificate.PairSemantics.raw5166step2 line 352
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5166 line 354
  67. def OAI.MUB6.Certificate.PairSemantics.raw5167 line 375
  68. def OAI.MUB6.Certificate.PairSemantics.raw5167step0 line 377
  69. def OAI.MUB6.Certificate.PairSemantics.raw5167step1 line 379
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical5167 line 381
  71. def OAI.MUB6.Certificate.PairSemantics.raw5168 line 397
  72. def OAI.MUB6.Certificate.PairSemantics.raw5168step0 line 399
  73. def OAI.MUB6.Certificate.PairSemantics.raw5168step1 line 401
  74. def OAI.MUB6.Certificate.PairSemantics.raw5168step2 line 403
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5168 line 405
  76. def OAI.MUB6.Certificate.PairSemantics.raw5169 line 426
  77. def OAI.MUB6.Certificate.PairSemantics.raw5169step0 line 428
  78. def OAI.MUB6.Certificate.PairSemantics.raw5169step1 line 430
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5169 line 432
  80. def OAI.MUB6.Certificate.PairSemantics.raw5170 line 448
  81. def OAI.MUB6.Certificate.PairSemantics.raw5170step0 line 450
  82. def OAI.MUB6.Certificate.PairSemantics.raw5170step1 line 452
  83. def OAI.MUB6.Certificate.PairSemantics.raw5170step2 line 454
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5170 line 456
  85. def OAI.MUB6.Certificate.PairSemantics.raw5171 line 477
  86. def OAI.MUB6.Certificate.PairSemantics.raw5171step0 line 479
  87. def OAI.MUB6.Certificate.PairSemantics.raw5171step1 line 481
  88. def OAI.MUB6.Certificate.PairSemantics.raw5171step2 line 483
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5171 line 485
  90. def OAI.MUB6.Certificate.PairSemantics.raw5172 line 505
  91. def OAI.MUB6.Certificate.PairSemantics.raw5172step0 line 507
  92. def OAI.MUB6.Certificate.PairSemantics.raw5172step1 line 509
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5172 line 511
  94. def OAI.MUB6.Certificate.PairSemantics.raw5173 line 526
  95. def OAI.MUB6.Certificate.PairSemantics.raw5173step0 line 528
  96. def OAI.MUB6.Certificate.PairSemantics.raw5173step1 line 530
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5173 line 532
  98. def OAI.MUB6.Certificate.PairSemantics.raw5174 line 547
  99. def OAI.MUB6.Certificate.PairSemantics.raw5174step0 line 549
  100. def OAI.MUB6.Certificate.PairSemantics.raw5174step1 line 551
  101. def OAI.MUB6.Certificate.PairSemantics.raw5174step2 line 553
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical5174 line 555
  103. def OAI.MUB6.Certificate.PairSemantics.raw5175 line 576
  104. def OAI.MUB6.Certificate.PairSemantics.raw5175step0 line 578
  105. def OAI.MUB6.Certificate.PairSemantics.raw5175step1 line 580
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical5175 line 582
  107. def OAI.MUB6.Certificate.PairSemantics.raw5176 line 598
  108. def OAI.MUB6.Certificate.PairSemantics.raw5176step0 line 600
  109. def OAI.MUB6.Certificate.PairSemantics.raw5176step1 line 602
  110. def OAI.MUB6.Certificate.PairSemantics.raw5176step2 line 604
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical5176 line 606
  112. def OAI.MUB6.Certificate.PairSemantics.raw5177 line 627
  113. def OAI.MUB6.Certificate.PairSemantics.raw5177step0 line 629
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical5177 line 631
  115. def OAI.MUB6.Certificate.PairSemantics.raw5178 line 642
  116. def OAI.MUB6.Certificate.PairSemantics.raw5178step0 line 644
  117. def OAI.MUB6.Certificate.PairSemantics.raw5178step1 line 646
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical5178 line 648
  119. def OAI.MUB6.Certificate.PairSemantics.raw5179 line 663
  120. def OAI.MUB6.Certificate.PairSemantics.raw5179step0 line 665
  121. def OAI.MUB6.Certificate.PairSemantics.raw5179step1 line 667
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical5179 line 669
  123. def OAI.MUB6.Certificate.PairSemantics.raw5180 line 685
  124. def OAI.MUB6.Certificate.PairSemantics.raw5180step0 line 687
  125. def OAI.MUB6.Certificate.PairSemantics.raw5180step1 line 689
  126. def OAI.MUB6.Certificate.PairSemantics.raw5180step2 line 691
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical5180 line 693
  128. def OAI.MUB6.Certificate.PairSemantics.raw5181 line 714
  129. def OAI.MUB6.Certificate.PairSemantics.raw5181step0 line 716
  130. def OAI.MUB6.Certificate.PairSemantics.raw5181step1 line 718
  131. theorem OAI.MUB6.Certificate.PairSemantics.canonical5181 line 720
  132. def OAI.MUB6.Certificate.PairSemantics.raw5182 line 735
  133. def OAI.MUB6.Certificate.PairSemantics.raw5182step0 line 737
  134. def OAI.MUB6.Certificate.PairSemantics.raw5182step1 line 739
  135. theorem OAI.MUB6.Certificate.PairSemantics.canonical5182 line 741
  136. def OAI.MUB6.Certificate.PairSemantics.raw5183 line 756
  137. def OAI.MUB6.Certificate.PairSemantics.raw5183step0 line 758
  138. theorem OAI.MUB6.Certificate.PairSemantics.canonical5183 line 760