OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical258.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8256 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8256step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8256 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw8257 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw8257step0 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw8257step1 line 36
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical8257 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw8258 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw8258step0 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw8258step1 line 56
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical8258 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw8259 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw8259step0 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw8259step1 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8259 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw8260 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw8260step0 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw8260step1 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8260 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw8261 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw8261step0 line 112
  22. def OAI.MUB6.Certificate.PairSemantics.raw8261step1 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw8261step2 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw8261step3 line 118
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8261 line 120
  26. def OAI.MUB6.Certificate.PairSemantics.raw8262 line 143
  27. def OAI.MUB6.Certificate.PairSemantics.raw8262step0 line 145
  28. def OAI.MUB6.Certificate.PairSemantics.raw8262step1 line 147
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8262 line 149
  30. def OAI.MUB6.Certificate.PairSemantics.raw8263 line 162
  31. def OAI.MUB6.Certificate.PairSemantics.raw8263step0 line 164
  32. def OAI.MUB6.Certificate.PairSemantics.raw8263step1 line 166
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8263 line 168
  34. def OAI.MUB6.Certificate.PairSemantics.raw8264 line 181
  35. def OAI.MUB6.Certificate.PairSemantics.raw8264step0 line 183
  36. def OAI.MUB6.Certificate.PairSemantics.raw8264step1 line 185
  37. def OAI.MUB6.Certificate.PairSemantics.raw8264step2 line 187
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8264 line 189
  39. def OAI.MUB6.Certificate.PairSemantics.raw8265 line 206
  40. def OAI.MUB6.Certificate.PairSemantics.raw8265step0 line 208
  41. def OAI.MUB6.Certificate.PairSemantics.raw8265step1 line 210
  42. def OAI.MUB6.Certificate.PairSemantics.raw8265step2 line 212
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical8265 line 214
  44. def OAI.MUB6.Certificate.PairSemantics.raw8266 line 231
  45. def OAI.MUB6.Certificate.PairSemantics.raw8266step0 line 233
  46. def OAI.MUB6.Certificate.PairSemantics.raw8266step1 line 235
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8266 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw8267 line 250
  49. def OAI.MUB6.Certificate.PairSemantics.raw8267step0 line 252
  50. def OAI.MUB6.Certificate.PairSemantics.raw8267step1 line 254
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8267 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw8268 line 269
  53. def OAI.MUB6.Certificate.PairSemantics.raw8268step0 line 271
  54. def OAI.MUB6.Certificate.PairSemantics.raw8268step1 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw8268step2 line 275
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8268 line 277
  57. def OAI.MUB6.Certificate.PairSemantics.raw8269 line 294
  58. def OAI.MUB6.Certificate.PairSemantics.raw8269step0 line 296
  59. def OAI.MUB6.Certificate.PairSemantics.raw8269step1 line 298
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical8269 line 300
  61. def OAI.MUB6.Certificate.PairSemantics.raw8270 line 313
  62. def OAI.MUB6.Certificate.PairSemantics.raw8270step0 line 315
  63. def OAI.MUB6.Certificate.PairSemantics.raw8270step1 line 317
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical8270 line 319
  65. def OAI.MUB6.Certificate.PairSemantics.raw8271 line 332
  66. def OAI.MUB6.Certificate.PairSemantics.raw8271step0 line 334
  67. def OAI.MUB6.Certificate.PairSemantics.raw8271step1 line 336
  68. def OAI.MUB6.Certificate.PairSemantics.raw8271step2 line 338
  69. def OAI.MUB6.Certificate.PairSemantics.raw8271step3 line 340
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8271 line 342
  71. def OAI.MUB6.Certificate.PairSemantics.raw8272 line 365
  72. def OAI.MUB6.Certificate.PairSemantics.raw8272step0 line 367
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8272 line 369
  74. def OAI.MUB6.Certificate.PairSemantics.raw8273 line 378
  75. def OAI.MUB6.Certificate.PairSemantics.raw8273step0 line 380
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8273 line 382
  77. def OAI.MUB6.Certificate.PairSemantics.raw8274 line 391
  78. def OAI.MUB6.Certificate.PairSemantics.raw8274step0 line 393
  79. def OAI.MUB6.Certificate.PairSemantics.raw8274step1 line 395
  80. def OAI.MUB6.Certificate.PairSemantics.raw8274step2 line 397
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8274 line 399
  82. def OAI.MUB6.Certificate.PairSemantics.raw8275 line 416
  83. def OAI.MUB6.Certificate.PairSemantics.raw8275step0 line 418
  84. def OAI.MUB6.Certificate.PairSemantics.raw8275step1 line 420
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8275 line 422
  86. def OAI.MUB6.Certificate.PairSemantics.raw8276 line 435
  87. def OAI.MUB6.Certificate.PairSemantics.raw8276step0 line 437
  88. def OAI.MUB6.Certificate.PairSemantics.raw8276step1 line 439
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8276 line 441
  90. def OAI.MUB6.Certificate.PairSemantics.raw8277 line 454
  91. def OAI.MUB6.Certificate.PairSemantics.raw8277step0 line 456
  92. def OAI.MUB6.Certificate.PairSemantics.raw8277step1 line 458
  93. def OAI.MUB6.Certificate.PairSemantics.raw8277step2 line 460
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8277 line 462
  95. def OAI.MUB6.Certificate.PairSemantics.raw8278 line 479
  96. def OAI.MUB6.Certificate.PairSemantics.raw8278step0 line 481
  97. def OAI.MUB6.Certificate.PairSemantics.raw8278step1 line 483
  98. def OAI.MUB6.Certificate.PairSemantics.raw8278step2 line 485
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8278 line 487
  100. def OAI.MUB6.Certificate.PairSemantics.raw8279 line 505
  101. def OAI.MUB6.Certificate.PairSemantics.raw8279step0 line 507
  102. def OAI.MUB6.Certificate.PairSemantics.raw8279step1 line 509
  103. def OAI.MUB6.Certificate.PairSemantics.raw8279step2 line 511
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8279 line 513
  105. def OAI.MUB6.Certificate.PairSemantics.raw8280 line 531
  106. def OAI.MUB6.Certificate.PairSemantics.raw8280step0 line 533
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8280 line 535
  108. def OAI.MUB6.Certificate.PairSemantics.raw8281 line 544
  109. def OAI.MUB6.Certificate.PairSemantics.raw8281step0 line 546
  110. def OAI.MUB6.Certificate.PairSemantics.raw8281step1 line 548
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical8281 line 550
  112. def OAI.MUB6.Certificate.PairSemantics.raw8282 line 563
  113. def OAI.MUB6.Certificate.PairSemantics.raw8282step0 line 565
  114. def OAI.MUB6.Certificate.PairSemantics.raw8282step1 line 567
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical8282 line 569
  116. def OAI.MUB6.Certificate.PairSemantics.raw8283 line 582
  117. def OAI.MUB6.Certificate.PairSemantics.raw8283step0 line 584
  118. def OAI.MUB6.Certificate.PairSemantics.raw8283step1 line 586
  119. def OAI.MUB6.Certificate.PairSemantics.raw8283step2 line 588
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8283 line 590
  121. def OAI.MUB6.Certificate.PairSemantics.raw8284 line 608
  122. def OAI.MUB6.Certificate.PairSemantics.raw8284step0 line 610
  123. def OAI.MUB6.Certificate.PairSemantics.raw8284step1 line 612
  124. def OAI.MUB6.Certificate.PairSemantics.raw8284step2 line 614
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical8284 line 616
  126. def OAI.MUB6.Certificate.PairSemantics.raw8285 line 634
  127. def OAI.MUB6.Certificate.PairSemantics.raw8285step0 line 636
  128. def OAI.MUB6.Certificate.PairSemantics.raw8285step1 line 638
  129. def OAI.MUB6.Certificate.PairSemantics.raw8285step2 line 640
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical8285 line 642
  131. def OAI.MUB6.Certificate.PairSemantics.raw8286 line 659
  132. def OAI.MUB6.Certificate.PairSemantics.raw8286step0 line 661
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical8286 line 663
  134. def OAI.MUB6.Certificate.PairSemantics.raw8287 line 673
  135. def OAI.MUB6.Certificate.PairSemantics.raw8287step0 line 675
  136. def OAI.MUB6.Certificate.PairSemantics.raw8287step1 line 677
  137. def OAI.MUB6.Certificate.PairSemantics.raw8287step2 line 679
  138. theorem OAI.MUB6.Certificate.PairSemantics.canonical8287 line 681