OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical278.lean

GitHub source file

150 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8896 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw8896step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw8896step1 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw8896step2 line 22
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical8896 line 24
  6. def OAI.MUB6.Certificate.PairSemantics.raw8897 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw8897step0 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw8897step1 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw8897step2 line 47
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8897 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw8898 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw8898step0 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw8898step1 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw8898step2 line 72
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8898 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw8899 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw8899step0 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw8899step1 line 95
  19. def OAI.MUB6.Certificate.PairSemantics.raw8899step2 line 97
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8899 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw8900 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw8900step0 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw8900step1 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw8900step2 line 122
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8900 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw8901 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw8901step0 line 143
  28. def OAI.MUB6.Certificate.PairSemantics.raw8901step1 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw8901step2 line 147
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8901 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw8902 line 166
  32. def OAI.MUB6.Certificate.PairSemantics.raw8902step0 line 168
  33. def OAI.MUB6.Certificate.PairSemantics.raw8902step1 line 170
  34. def OAI.MUB6.Certificate.PairSemantics.raw8902step2 line 172
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8902 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw8903 line 191
  37. def OAI.MUB6.Certificate.PairSemantics.raw8903step0 line 193
  38. def OAI.MUB6.Certificate.PairSemantics.raw8903step1 line 195
  39. def OAI.MUB6.Certificate.PairSemantics.raw8903step2 line 197
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8903 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw8904 line 216
  42. def OAI.MUB6.Certificate.PairSemantics.raw8904step0 line 218
  43. def OAI.MUB6.Certificate.PairSemantics.raw8904step1 line 220
  44. def OAI.MUB6.Certificate.PairSemantics.raw8904step2 line 222
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8904 line 224
  46. def OAI.MUB6.Certificate.PairSemantics.raw8905 line 241
  47. def OAI.MUB6.Certificate.PairSemantics.raw8905step0 line 243
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8905 line 245
  49. def OAI.MUB6.Certificate.PairSemantics.raw8906 line 254
  50. def OAI.MUB6.Certificate.PairSemantics.raw8906step0 line 256
  51. def OAI.MUB6.Certificate.PairSemantics.raw8906step1 line 258
  52. def OAI.MUB6.Certificate.PairSemantics.raw8906step2 line 260
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8906 line 262
  54. def OAI.MUB6.Certificate.PairSemantics.raw8907 line 279
  55. def OAI.MUB6.Certificate.PairSemantics.raw8907step0 line 281
  56. def OAI.MUB6.Certificate.PairSemantics.raw8907step1 line 283
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8907 line 285
  58. def OAI.MUB6.Certificate.PairSemantics.raw8908 line 298
  59. def OAI.MUB6.Certificate.PairSemantics.raw8908step0 line 300
  60. def OAI.MUB6.Certificate.PairSemantics.raw8908step1 line 302
  61. def OAI.MUB6.Certificate.PairSemantics.raw8908step2 line 304
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8908 line 306
  63. def OAI.MUB6.Certificate.PairSemantics.raw8909 line 323
  64. def OAI.MUB6.Certificate.PairSemantics.raw8909step0 line 325
  65. def OAI.MUB6.Certificate.PairSemantics.raw8909step1 line 327
  66. def OAI.MUB6.Certificate.PairSemantics.raw8909step2 line 329
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical8909 line 331
  68. def OAI.MUB6.Certificate.PairSemantics.raw8910 line 348
  69. def OAI.MUB6.Certificate.PairSemantics.raw8910step0 line 350
  70. def OAI.MUB6.Certificate.PairSemantics.raw8910step1 line 352
  71. def OAI.MUB6.Certificate.PairSemantics.raw8910step2 line 354
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical8910 line 356
  73. def OAI.MUB6.Certificate.PairSemantics.raw8911 line 373
  74. def OAI.MUB6.Certificate.PairSemantics.raw8911step0 line 375
  75. def OAI.MUB6.Certificate.PairSemantics.raw8911step1 line 377
  76. def OAI.MUB6.Certificate.PairSemantics.raw8911step2 line 379
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8911 line 381
  78. def OAI.MUB6.Certificate.PairSemantics.raw8912 line 398
  79. def OAI.MUB6.Certificate.PairSemantics.raw8912step0 line 400
  80. def OAI.MUB6.Certificate.PairSemantics.raw8912step1 line 402
  81. def OAI.MUB6.Certificate.PairSemantics.raw8912step2 line 404
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8912 line 406
  83. def OAI.MUB6.Certificate.PairSemantics.raw8913 line 423
  84. def OAI.MUB6.Certificate.PairSemantics.raw8913step0 line 425
  85. def OAI.MUB6.Certificate.PairSemantics.raw8913step1 line 427
  86. def OAI.MUB6.Certificate.PairSemantics.raw8913step2 line 429
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical8913 line 431
  88. def OAI.MUB6.Certificate.PairSemantics.raw8914 line 448
  89. def OAI.MUB6.Certificate.PairSemantics.raw8914step0 line 450
  90. def OAI.MUB6.Certificate.PairSemantics.raw8914step1 line 452
  91. def OAI.MUB6.Certificate.PairSemantics.raw8914step2 line 454
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical8914 line 456
  93. def OAI.MUB6.Certificate.PairSemantics.raw8915 line 474
  94. def OAI.MUB6.Certificate.PairSemantics.raw8915step0 line 476
  95. def OAI.MUB6.Certificate.PairSemantics.raw8915step1 line 478
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8915 line 480
  97. def OAI.MUB6.Certificate.PairSemantics.raw8916 line 493
  98. def OAI.MUB6.Certificate.PairSemantics.raw8916step0 line 495
  99. def OAI.MUB6.Certificate.PairSemantics.raw8916step1 line 497
  100. def OAI.MUB6.Certificate.PairSemantics.raw8916step2 line 499
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8916 line 501
  102. def OAI.MUB6.Certificate.PairSemantics.raw8917 line 519
  103. def OAI.MUB6.Certificate.PairSemantics.raw8917step0 line 521
  104. def OAI.MUB6.Certificate.PairSemantics.raw8917step1 line 523
  105. def OAI.MUB6.Certificate.PairSemantics.raw8917step2 line 525
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8917 line 527
  107. def OAI.MUB6.Certificate.PairSemantics.raw8918 line 544
  108. def OAI.MUB6.Certificate.PairSemantics.raw8918step0 line 546
  109. def OAI.MUB6.Certificate.PairSemantics.raw8918step1 line 548
  110. def OAI.MUB6.Certificate.PairSemantics.raw8918step2 line 550
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical8918 line 552
  112. def OAI.MUB6.Certificate.PairSemantics.raw8919 line 570
  113. def OAI.MUB6.Certificate.PairSemantics.raw8919step0 line 572
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8919 line 574
  115. def OAI.MUB6.Certificate.PairSemantics.raw8920 line 583
  116. def OAI.MUB6.Certificate.PairSemantics.raw8920step0 line 585
  117. def OAI.MUB6.Certificate.PairSemantics.raw8920step1 line 587
  118. def OAI.MUB6.Certificate.PairSemantics.raw8920step2 line 589
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical8920 line 591
  120. def OAI.MUB6.Certificate.PairSemantics.raw8921 line 609
  121. def OAI.MUB6.Certificate.PairSemantics.raw8921step0 line 611
  122. def OAI.MUB6.Certificate.PairSemantics.raw8921step1 line 613
  123. def OAI.MUB6.Certificate.PairSemantics.raw8921step2 line 615
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical8921 line 617
  125. def OAI.MUB6.Certificate.PairSemantics.raw8922 line 634
  126. def OAI.MUB6.Certificate.PairSemantics.raw8922step0 line 636
  127. def OAI.MUB6.Certificate.PairSemantics.raw8922step1 line 638
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical8922 line 640
  129. def OAI.MUB6.Certificate.PairSemantics.raw8923 line 654
  130. def OAI.MUB6.Certificate.PairSemantics.raw8923step0 line 656
  131. def OAI.MUB6.Certificate.PairSemantics.raw8923step1 line 658
  132. theorem OAI.MUB6.Certificate.PairSemantics.canonical8923 line 660
  133. def OAI.MUB6.Certificate.PairSemantics.raw8924 line 674
  134. def OAI.MUB6.Certificate.PairSemantics.raw8924step0 line 676
  135. def OAI.MUB6.Certificate.PairSemantics.raw8924step1 line 678
  136. def OAI.MUB6.Certificate.PairSemantics.raw8924step2 line 680
  137. theorem OAI.MUB6.Certificate.PairSemantics.canonical8924 line 682
  138. def OAI.MUB6.Certificate.PairSemantics.raw8925 line 700
  139. def OAI.MUB6.Certificate.PairSemantics.raw8925step0 line 702
  140. def OAI.MUB6.Certificate.PairSemantics.raw8925step1 line 704
  141. def OAI.MUB6.Certificate.PairSemantics.raw8925step2 line 706
  142. theorem OAI.MUB6.Certificate.PairSemantics.canonical8925 line 708
  143. def OAI.MUB6.Certificate.PairSemantics.raw8926 line 725
  144. def OAI.MUB6.Certificate.PairSemantics.raw8926step0 line 727
  145. def OAI.MUB6.Certificate.PairSemantics.raw8926step1 line 729
  146. theorem OAI.MUB6.Certificate.PairSemantics.canonical8926 line 731
  147. def OAI.MUB6.Certificate.PairSemantics.raw8927 line 744
  148. def OAI.MUB6.Certificate.PairSemantics.raw8927step0 line 746
  149. def OAI.MUB6.Certificate.PairSemantics.raw8927step1 line 748
  150. theorem OAI.MUB6.Certificate.PairSemantics.canonical8927 line 750