OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical259.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8288 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw8288step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw8288step1 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw8288step2 line 26
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical8288 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw8289 line 45
  7. def OAI.MUB6.Certificate.PairSemantics.raw8289step0 line 47
  8. def OAI.MUB6.Certificate.PairSemantics.raw8289step1 line 49
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8289 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw8290 line 65
  11. def OAI.MUB6.Certificate.PairSemantics.raw8290step0 line 67
  12. def OAI.MUB6.Certificate.PairSemantics.raw8290step1 line 69
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical8290 line 71
  14. def OAI.MUB6.Certificate.PairSemantics.raw8291 line 84
  15. def OAI.MUB6.Certificate.PairSemantics.raw8291step0 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw8291step1 line 88
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8291 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw8292 line 103
  19. def OAI.MUB6.Certificate.PairSemantics.raw8292step0 line 105
  20. def OAI.MUB6.Certificate.PairSemantics.raw8292step1 line 107
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical8292 line 109
  22. def OAI.MUB6.Certificate.PairSemantics.raw8293 line 122
  23. def OAI.MUB6.Certificate.PairSemantics.raw8293step0 line 124
  24. def OAI.MUB6.Certificate.PairSemantics.raw8293step1 line 126
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8293 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw8294 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw8294step0 line 143
  28. def OAI.MUB6.Certificate.PairSemantics.raw8294step1 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw8294step2 line 147
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8294 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw8295 line 166
  32. def OAI.MUB6.Certificate.PairSemantics.raw8295step0 line 168
  33. def OAI.MUB6.Certificate.PairSemantics.raw8295step1 line 170
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8295 line 172
  35. def OAI.MUB6.Certificate.PairSemantics.raw8296 line 186
  36. def OAI.MUB6.Certificate.PairSemantics.raw8296step0 line 188
  37. def OAI.MUB6.Certificate.PairSemantics.raw8296step1 line 190
  38. def OAI.MUB6.Certificate.PairSemantics.raw8296step2 line 192
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8296 line 194
  40. def OAI.MUB6.Certificate.PairSemantics.raw8297 line 212
  41. def OAI.MUB6.Certificate.PairSemantics.raw8297step0 line 214
  42. def OAI.MUB6.Certificate.PairSemantics.raw8297step1 line 216
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical8297 line 218
  44. def OAI.MUB6.Certificate.PairSemantics.raw8298 line 231
  45. def OAI.MUB6.Certificate.PairSemantics.raw8298step0 line 233
  46. def OAI.MUB6.Certificate.PairSemantics.raw8298step1 line 235
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8298 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw8299 line 250
  49. def OAI.MUB6.Certificate.PairSemantics.raw8299step0 line 252
  50. def OAI.MUB6.Certificate.PairSemantics.raw8299step1 line 254
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8299 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw8300 line 269
  53. def OAI.MUB6.Certificate.PairSemantics.raw8300step0 line 271
  54. def OAI.MUB6.Certificate.PairSemantics.raw8300step1 line 273
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8300 line 275
  56. def OAI.MUB6.Certificate.PairSemantics.raw8301 line 289
  57. def OAI.MUB6.Certificate.PairSemantics.raw8301step0 line 291
  58. def OAI.MUB6.Certificate.PairSemantics.raw8301step1 line 293
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8301 line 295
  60. def OAI.MUB6.Certificate.PairSemantics.raw8302 line 309
  61. def OAI.MUB6.Certificate.PairSemantics.raw8302step0 line 311
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8302 line 313
  63. def OAI.MUB6.Certificate.PairSemantics.raw8303 line 323
  64. def OAI.MUB6.Certificate.PairSemantics.raw8303step0 line 325
  65. def OAI.MUB6.Certificate.PairSemantics.raw8303step1 line 327
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8303 line 329
  67. def OAI.MUB6.Certificate.PairSemantics.raw8304 line 342
  68. def OAI.MUB6.Certificate.PairSemantics.raw8304step0 line 344
  69. def OAI.MUB6.Certificate.PairSemantics.raw8304step1 line 346
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8304 line 348
  71. def OAI.MUB6.Certificate.PairSemantics.raw8305 line 362
  72. def OAI.MUB6.Certificate.PairSemantics.raw8305step0 line 364
  73. def OAI.MUB6.Certificate.PairSemantics.raw8305step1 line 366
  74. def OAI.MUB6.Certificate.PairSemantics.raw8305step2 line 368
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8305 line 370
  76. def OAI.MUB6.Certificate.PairSemantics.raw8306 line 388
  77. def OAI.MUB6.Certificate.PairSemantics.raw8306step0 line 390
  78. def OAI.MUB6.Certificate.PairSemantics.raw8306step1 line 392
  79. def OAI.MUB6.Certificate.PairSemantics.raw8306step2 line 394
  80. def OAI.MUB6.Certificate.PairSemantics.raw8306step3 line 396
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8306 line 398
  82. def OAI.MUB6.Certificate.PairSemantics.raw8307 line 420
  83. def OAI.MUB6.Certificate.PairSemantics.raw8307step0 line 422
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical8307 line 424
  85. def OAI.MUB6.Certificate.PairSemantics.raw8308 line 433
  86. def OAI.MUB6.Certificate.PairSemantics.raw8308step0 line 435
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical8308 line 437
  88. def OAI.MUB6.Certificate.PairSemantics.raw8309 line 446
  89. def OAI.MUB6.Certificate.PairSemantics.raw8309step0 line 448
  90. def OAI.MUB6.Certificate.PairSemantics.raw8309step1 line 450
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8309 line 452
  92. def OAI.MUB6.Certificate.PairSemantics.raw8310 line 465
  93. def OAI.MUB6.Certificate.PairSemantics.raw8310step0 line 467
  94. def OAI.MUB6.Certificate.PairSemantics.raw8310step1 line 469
  95. def OAI.MUB6.Certificate.PairSemantics.raw8310step2 line 471
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8310 line 473
  97. def OAI.MUB6.Certificate.PairSemantics.raw8311 line 490
  98. def OAI.MUB6.Certificate.PairSemantics.raw8311step0 line 492
  99. def OAI.MUB6.Certificate.PairSemantics.raw8311step1 line 494
  100. def OAI.MUB6.Certificate.PairSemantics.raw8311step2 line 496
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8311 line 498
  102. def OAI.MUB6.Certificate.PairSemantics.raw8312 line 516
  103. def OAI.MUB6.Certificate.PairSemantics.raw8312step0 line 518
  104. def OAI.MUB6.Certificate.PairSemantics.raw8312step1 line 520
  105. def OAI.MUB6.Certificate.PairSemantics.raw8312step2 line 522
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8312 line 524
  107. def OAI.MUB6.Certificate.PairSemantics.raw8313 line 541
  108. def OAI.MUB6.Certificate.PairSemantics.raw8313step0 line 543
  109. def OAI.MUB6.Certificate.PairSemantics.raw8313step1 line 545
  110. def OAI.MUB6.Certificate.PairSemantics.raw8313step2 line 547
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical8313 line 549
  112. def OAI.MUB6.Certificate.PairSemantics.raw8314 line 567
  113. def OAI.MUB6.Certificate.PairSemantics.raw8314step0 line 569
  114. def OAI.MUB6.Certificate.PairSemantics.raw8314step1 line 571
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical8314 line 573
  116. def OAI.MUB6.Certificate.PairSemantics.raw8315 line 586
  117. def OAI.MUB6.Certificate.PairSemantics.raw8315step0 line 588
  118. def OAI.MUB6.Certificate.PairSemantics.raw8315step1 line 590
  119. def OAI.MUB6.Certificate.PairSemantics.raw8315step2 line 592
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8315 line 594
  121. def OAI.MUB6.Certificate.PairSemantics.raw8316 line 612
  122. def OAI.MUB6.Certificate.PairSemantics.raw8316step0 line 614
  123. def OAI.MUB6.Certificate.PairSemantics.raw8316step1 line 616
  124. def OAI.MUB6.Certificate.PairSemantics.raw8316step2 line 618
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical8316 line 620
  126. def OAI.MUB6.Certificate.PairSemantics.raw8317 line 638
  127. def OAI.MUB6.Certificate.PairSemantics.raw8317step0 line 640
  128. def OAI.MUB6.Certificate.PairSemantics.raw8317step1 line 642
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical8317 line 644
  130. def OAI.MUB6.Certificate.PairSemantics.raw8318 line 658
  131. def OAI.MUB6.Certificate.PairSemantics.raw8318step0 line 660
  132. def OAI.MUB6.Certificate.PairSemantics.raw8318step1 line 662
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical8318 line 664
  134. def OAI.MUB6.Certificate.PairSemantics.raw8319 line 677
  135. def OAI.MUB6.Certificate.PairSemantics.raw8319step0 line 679
  136. theorem OAI.MUB6.Certificate.PairSemantics.canonical8319 line 681