OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical81.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2592 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw2592step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw2592step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2592 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw2593 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw2593step0 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw2593step1 line 40
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2593 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw2594 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw2594step0 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw2594step1 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2594 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw2595 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw2595step0 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2595 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw2596 line 87
  17. def OAI.MUB6.Certificate.PairSemantics.raw2596step0 line 89
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2596 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw2597 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw2597step0 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw2597step1 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw2597step2 line 106
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2597 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw2598 line 125
  25. def OAI.MUB6.Certificate.PairSemantics.raw2598step0 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw2598step1 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw2598step2 line 131
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2598 line 133
  29. def OAI.MUB6.Certificate.PairSemantics.raw2599 line 150
  30. def OAI.MUB6.Certificate.PairSemantics.raw2599step0 line 152
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2599 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw2600 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw2600step0 line 165
  34. def OAI.MUB6.Certificate.PairSemantics.raw2600step1 line 167
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical2600 line 169
  36. def OAI.MUB6.Certificate.PairSemantics.raw2601 line 182
  37. def OAI.MUB6.Certificate.PairSemantics.raw2601step0 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw2601step1 line 186
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2601 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw2602 line 201
  41. def OAI.MUB6.Certificate.PairSemantics.raw2602step0 line 203
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2602 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw2603 line 214
  44. def OAI.MUB6.Certificate.PairSemantics.raw2603step0 line 216
  45. def OAI.MUB6.Certificate.PairSemantics.raw2603step1 line 218
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2603 line 220
  47. def OAI.MUB6.Certificate.PairSemantics.raw2604 line 233
  48. def OAI.MUB6.Certificate.PairSemantics.raw2604step0 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw2604step1 line 237
  50. def OAI.MUB6.Certificate.PairSemantics.raw2604step2 line 239
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2604 line 241
  52. def OAI.MUB6.Certificate.PairSemantics.raw2605 line 258
  53. def OAI.MUB6.Certificate.PairSemantics.raw2605step0 line 260
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2605 line 262
  55. def OAI.MUB6.Certificate.PairSemantics.raw2606 line 271
  56. def OAI.MUB6.Certificate.PairSemantics.raw2606step0 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw2606step1 line 275
  58. def OAI.MUB6.Certificate.PairSemantics.raw2606step2 line 277
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2606 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw2607 line 296
  61. def OAI.MUB6.Certificate.PairSemantics.raw2607step0 line 298
  62. def OAI.MUB6.Certificate.PairSemantics.raw2607step1 line 300
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2607 line 302
  64. def OAI.MUB6.Certificate.PairSemantics.raw2608 line 315
  65. def OAI.MUB6.Certificate.PairSemantics.raw2608step0 line 317
  66. def OAI.MUB6.Certificate.PairSemantics.raw2608step1 line 319
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2608 line 321
  68. def OAI.MUB6.Certificate.PairSemantics.raw2609 line 334
  69. def OAI.MUB6.Certificate.PairSemantics.raw2609step0 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw2609step1 line 338
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2609 line 340
  72. def OAI.MUB6.Certificate.PairSemantics.raw2610 line 353
  73. def OAI.MUB6.Certificate.PairSemantics.raw2610step0 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw2610step1 line 357
  75. def OAI.MUB6.Certificate.PairSemantics.raw2610step2 line 359
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2610 line 361
  77. def OAI.MUB6.Certificate.PairSemantics.raw2611 line 379
  78. def OAI.MUB6.Certificate.PairSemantics.raw2611step0 line 381
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2611 line 383
  80. def OAI.MUB6.Certificate.PairSemantics.raw2612 line 392
  81. def OAI.MUB6.Certificate.PairSemantics.raw2612step0 line 394
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2612 line 396
  83. def OAI.MUB6.Certificate.PairSemantics.raw2613 line 405
  84. def OAI.MUB6.Certificate.PairSemantics.raw2613step0 line 407
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical2613 line 409
  86. def OAI.MUB6.Certificate.PairSemantics.raw2614 line 418
  87. def OAI.MUB6.Certificate.PairSemantics.raw2614step0 line 420
  88. def OAI.MUB6.Certificate.PairSemantics.raw2614step1 line 422
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2614 line 424
  90. def OAI.MUB6.Certificate.PairSemantics.raw2615 line 437
  91. def OAI.MUB6.Certificate.PairSemantics.raw2615step0 line 439
  92. def OAI.MUB6.Certificate.PairSemantics.raw2615step1 line 441
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical2615 line 443
  94. def OAI.MUB6.Certificate.PairSemantics.raw2616 line 456
  95. def OAI.MUB6.Certificate.PairSemantics.raw2616step0 line 458
  96. def OAI.MUB6.Certificate.PairSemantics.raw2616step1 line 460
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical2616 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw2617 line 475
  99. def OAI.MUB6.Certificate.PairSemantics.raw2617step0 line 477
  100. def OAI.MUB6.Certificate.PairSemantics.raw2617step1 line 479
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical2617 line 481
  102. def OAI.MUB6.Certificate.PairSemantics.raw2618 line 494
  103. def OAI.MUB6.Certificate.PairSemantics.raw2618step0 line 496
  104. def OAI.MUB6.Certificate.PairSemantics.raw2618step1 line 498
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical2618 line 500
  106. def OAI.MUB6.Certificate.PairSemantics.raw2619 line 513
  107. def OAI.MUB6.Certificate.PairSemantics.raw2619step0 line 515
  108. def OAI.MUB6.Certificate.PairSemantics.raw2619step1 line 517
  109. def OAI.MUB6.Certificate.PairSemantics.raw2619step2 line 519
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical2619 line 521
  111. def OAI.MUB6.Certificate.PairSemantics.raw2620 line 538
  112. def OAI.MUB6.Certificate.PairSemantics.raw2620step0 line 540
  113. def OAI.MUB6.Certificate.PairSemantics.raw2620step1 line 542
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical2620 line 544
  115. def OAI.MUB6.Certificate.PairSemantics.raw2621 line 557
  116. def OAI.MUB6.Certificate.PairSemantics.raw2621step0 line 559
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical2621 line 561
  118. def OAI.MUB6.Certificate.PairSemantics.raw2622 line 570
  119. def OAI.MUB6.Certificate.PairSemantics.raw2622step0 line 572
  120. def OAI.MUB6.Certificate.PairSemantics.raw2622step1 line 574
  121. def OAI.MUB6.Certificate.PairSemantics.raw2622step2 line 576
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical2622 line 578
  123. def OAI.MUB6.Certificate.PairSemantics.raw2623 line 595
  124. def OAI.MUB6.Certificate.PairSemantics.raw2623step0 line 597
  125. def OAI.MUB6.Certificate.PairSemantics.raw2623step1 line 599
  126. def OAI.MUB6.Certificate.PairSemantics.raw2623step2 line 601
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical2623 line 603