OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical257.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8224 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8224step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw8224step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8224 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw8225 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw8225step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw8225step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8225 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw8226 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw8226step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw8226step1 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw8226step2 line 63
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical8226 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw8227 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw8227step0 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw8227step1 line 86
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8227 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw8228 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw8228step0 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw8228step1 line 105
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical8228 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw8229 line 120
  23. def OAI.MUB6.Certificate.PairSemantics.raw8229step0 line 122
  24. def OAI.MUB6.Certificate.PairSemantics.raw8229step1 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw8229step2 line 126
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical8229 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw8230 line 145
  28. def OAI.MUB6.Certificate.PairSemantics.raw8230step0 line 147
  29. def OAI.MUB6.Certificate.PairSemantics.raw8230step1 line 149
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8230 line 151
  31. def OAI.MUB6.Certificate.PairSemantics.raw8231 line 164
  32. def OAI.MUB6.Certificate.PairSemantics.raw8231step0 line 166
  33. def OAI.MUB6.Certificate.PairSemantics.raw8231step1 line 168
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8231 line 170
  35. def OAI.MUB6.Certificate.PairSemantics.raw8232 line 183
  36. def OAI.MUB6.Certificate.PairSemantics.raw8232step0 line 185
  37. def OAI.MUB6.Certificate.PairSemantics.raw8232step1 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw8232step2 line 189
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8232 line 191
  40. def OAI.MUB6.Certificate.PairSemantics.raw8233 line 208
  41. def OAI.MUB6.Certificate.PairSemantics.raw8233step0 line 210
  42. def OAI.MUB6.Certificate.PairSemantics.raw8233step1 line 212
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical8233 line 214
  44. def OAI.MUB6.Certificate.PairSemantics.raw8234 line 227
  45. def OAI.MUB6.Certificate.PairSemantics.raw8234step0 line 229
  46. def OAI.MUB6.Certificate.PairSemantics.raw8234step1 line 231
  47. def OAI.MUB6.Certificate.PairSemantics.raw8234step2 line 233
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8234 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw8235 line 252
  50. def OAI.MUB6.Certificate.PairSemantics.raw8235step0 line 254
  51. def OAI.MUB6.Certificate.PairSemantics.raw8235step1 line 256
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical8235 line 258
  53. def OAI.MUB6.Certificate.PairSemantics.raw8236 line 271
  54. def OAI.MUB6.Certificate.PairSemantics.raw8236step0 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw8236step1 line 275
  56. def OAI.MUB6.Certificate.PairSemantics.raw8236step2 line 277
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8236 line 279
  58. def OAI.MUB6.Certificate.PairSemantics.raw8237 line 296
  59. def OAI.MUB6.Certificate.PairSemantics.raw8237step0 line 298
  60. def OAI.MUB6.Certificate.PairSemantics.raw8237step1 line 300
  61. def OAI.MUB6.Certificate.PairSemantics.raw8237step2 line 302
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8237 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw8238 line 321
  64. def OAI.MUB6.Certificate.PairSemantics.raw8238step0 line 323
  65. def OAI.MUB6.Certificate.PairSemantics.raw8238step1 line 325
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8238 line 327
  67. def OAI.MUB6.Certificate.PairSemantics.raw8239 line 340
  68. def OAI.MUB6.Certificate.PairSemantics.raw8239step0 line 342
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8239 line 344
  70. def OAI.MUB6.Certificate.PairSemantics.raw8240 line 353
  71. def OAI.MUB6.Certificate.PairSemantics.raw8240step0 line 355
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical8240 line 357
  73. def OAI.MUB6.Certificate.PairSemantics.raw8241 line 366
  74. def OAI.MUB6.Certificate.PairSemantics.raw8241step0 line 368
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8241 line 370
  76. def OAI.MUB6.Certificate.PairSemantics.raw8242 line 379
  77. def OAI.MUB6.Certificate.PairSemantics.raw8242step0 line 381
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical8242 line 383
  79. def OAI.MUB6.Certificate.PairSemantics.raw8243 line 392
  80. def OAI.MUB6.Certificate.PairSemantics.raw8243step0 line 394
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8243 line 396
  82. def OAI.MUB6.Certificate.PairSemantics.raw8244 line 405
  83. def OAI.MUB6.Certificate.PairSemantics.raw8244step0 line 407
  84. def OAI.MUB6.Certificate.PairSemantics.raw8244step1 line 409
  85. def OAI.MUB6.Certificate.PairSemantics.raw8244step2 line 411
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8244 line 413
  87. def OAI.MUB6.Certificate.PairSemantics.raw8245 line 430
  88. def OAI.MUB6.Certificate.PairSemantics.raw8245step0 line 432
  89. def OAI.MUB6.Certificate.PairSemantics.raw8245step1 line 434
  90. def OAI.MUB6.Certificate.PairSemantics.raw8245step2 line 436
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8245 line 438
  92. def OAI.MUB6.Certificate.PairSemantics.raw8246 line 455
  93. def OAI.MUB6.Certificate.PairSemantics.raw8246step0 line 457
  94. def OAI.MUB6.Certificate.PairSemantics.raw8246step1 line 459
  95. def OAI.MUB6.Certificate.PairSemantics.raw8246step2 line 461
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8246 line 463
  97. def OAI.MUB6.Certificate.PairSemantics.raw8247 line 480
  98. def OAI.MUB6.Certificate.PairSemantics.raw8247step0 line 482
  99. def OAI.MUB6.Certificate.PairSemantics.raw8247step1 line 484
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical8247 line 486
  101. def OAI.MUB6.Certificate.PairSemantics.raw8248 line 500
  102. def OAI.MUB6.Certificate.PairSemantics.raw8248step0 line 502
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical8248 line 504
  104. def OAI.MUB6.Certificate.PairSemantics.raw8249 line 513
  105. def OAI.MUB6.Certificate.PairSemantics.raw8249step0 line 515
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8249 line 517
  107. def OAI.MUB6.Certificate.PairSemantics.raw8250 line 526
  108. def OAI.MUB6.Certificate.PairSemantics.raw8250step0 line 528
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical8250 line 530
  110. def OAI.MUB6.Certificate.PairSemantics.raw8251 line 539
  111. def OAI.MUB6.Certificate.PairSemantics.raw8251step0 line 541
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical8251 line 543
  113. def OAI.MUB6.Certificate.PairSemantics.raw8252 line 552
  114. def OAI.MUB6.Certificate.PairSemantics.raw8252step0 line 554
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical8252 line 556
  116. def OAI.MUB6.Certificate.PairSemantics.raw8253 line 565
  117. def OAI.MUB6.Certificate.PairSemantics.raw8253step0 line 567
  118. def OAI.MUB6.Certificate.PairSemantics.raw8253step1 line 569
  119. def OAI.MUB6.Certificate.PairSemantics.raw8253step2 line 571
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8253 line 573
  121. def OAI.MUB6.Certificate.PairSemantics.raw8254 line 591
  122. def OAI.MUB6.Certificate.PairSemantics.raw8254step0 line 593
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical8254 line 595
  124. def OAI.MUB6.Certificate.PairSemantics.raw8255 line 604
  125. def OAI.MUB6.Certificate.PairSemantics.raw8255step0 line 606
  126. def OAI.MUB6.Certificate.PairSemantics.raw8255step1 line 608
  127. def OAI.MUB6.Certificate.PairSemantics.raw8255step2 line 610
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical8255 line 612