OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical254.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8128 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw8128step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw8128step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8128 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw8129 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw8129step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw8129step1 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8129 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw8130 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw8130step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw8130step1 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw8130step2 line 66
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical8130 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw8131 line 86
  15. def OAI.MUB6.Certificate.PairSemantics.raw8131step0 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw8131step1 line 90
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8131 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw8132 line 105
  19. def OAI.MUB6.Certificate.PairSemantics.raw8132step0 line 107
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8132 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw8133 line 118
  22. def OAI.MUB6.Certificate.PairSemantics.raw8133step0 line 120
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8133 line 122
  24. def OAI.MUB6.Certificate.PairSemantics.raw8134 line 131
  25. def OAI.MUB6.Certificate.PairSemantics.raw8134step0 line 133
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical8134 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw8135 line 144
  28. def OAI.MUB6.Certificate.PairSemantics.raw8135step0 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw8135step1 line 148
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8135 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw8136 line 163
  32. def OAI.MUB6.Certificate.PairSemantics.raw8136step0 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw8136step1 line 167
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8136 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw8137 line 184
  36. def OAI.MUB6.Certificate.PairSemantics.raw8137step0 line 186
  37. def OAI.MUB6.Certificate.PairSemantics.raw8137step1 line 188
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8137 line 190
  39. def OAI.MUB6.Certificate.PairSemantics.raw8138 line 204
  40. def OAI.MUB6.Certificate.PairSemantics.raw8138step0 line 206
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical8138 line 208
  42. def OAI.MUB6.Certificate.PairSemantics.raw8139 line 217
  43. def OAI.MUB6.Certificate.PairSemantics.raw8139step0 line 219
  44. def OAI.MUB6.Certificate.PairSemantics.raw8139step1 line 221
  45. def OAI.MUB6.Certificate.PairSemantics.raw8139step2 line 223
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical8139 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw8140 line 243
  48. def OAI.MUB6.Certificate.PairSemantics.raw8140step0 line 245
  49. def OAI.MUB6.Certificate.PairSemantics.raw8140step1 line 247
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8140 line 249
  51. def OAI.MUB6.Certificate.PairSemantics.raw8141 line 262
  52. def OAI.MUB6.Certificate.PairSemantics.raw8141step0 line 264
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8141 line 266
  54. def OAI.MUB6.Certificate.PairSemantics.raw8142 line 275
  55. def OAI.MUB6.Certificate.PairSemantics.raw8142step0 line 277
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8142 line 279
  57. def OAI.MUB6.Certificate.PairSemantics.raw8143 line 288
  58. def OAI.MUB6.Certificate.PairSemantics.raw8143step0 line 290
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8143 line 292
  60. def OAI.MUB6.Certificate.PairSemantics.raw8144 line 301
  61. def OAI.MUB6.Certificate.PairSemantics.raw8144step0 line 303
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8144 line 305
  63. def OAI.MUB6.Certificate.PairSemantics.raw8145 line 314
  64. def OAI.MUB6.Certificate.PairSemantics.raw8145step0 line 316
  65. def OAI.MUB6.Certificate.PairSemantics.raw8145step1 line 318
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8145 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw8146 line 333
  68. def OAI.MUB6.Certificate.PairSemantics.raw8146step0 line 335
  69. def OAI.MUB6.Certificate.PairSemantics.raw8146step1 line 337
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8146 line 339
  71. def OAI.MUB6.Certificate.PairSemantics.raw8147 line 352
  72. def OAI.MUB6.Certificate.PairSemantics.raw8147step0 line 354
  73. def OAI.MUB6.Certificate.PairSemantics.raw8147step1 line 356
  74. def OAI.MUB6.Certificate.PairSemantics.raw8147step2 line 358
  75. def OAI.MUB6.Certificate.PairSemantics.raw8147step3 line 360
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8147 line 362
  77. def OAI.MUB6.Certificate.PairSemantics.raw8148 line 385
  78. def OAI.MUB6.Certificate.PairSemantics.raw8148step0 line 387
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8148 line 389
  80. def OAI.MUB6.Certificate.PairSemantics.raw8149 line 398
  81. def OAI.MUB6.Certificate.PairSemantics.raw8149step0 line 400
  82. def OAI.MUB6.Certificate.PairSemantics.raw8149step1 line 402
  83. def OAI.MUB6.Certificate.PairSemantics.raw8149step2 line 404
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical8149 line 406
  85. def OAI.MUB6.Certificate.PairSemantics.raw8150 line 425
  86. def OAI.MUB6.Certificate.PairSemantics.raw8150step0 line 427
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical8150 line 429
  88. def OAI.MUB6.Certificate.PairSemantics.raw8151 line 438
  89. def OAI.MUB6.Certificate.PairSemantics.raw8151step0 line 440
  90. def OAI.MUB6.Certificate.PairSemantics.raw8151step1 line 442
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8151 line 444
  92. def OAI.MUB6.Certificate.PairSemantics.raw8152 line 457
  93. def OAI.MUB6.Certificate.PairSemantics.raw8152step0 line 459
  94. def OAI.MUB6.Certificate.PairSemantics.raw8152step1 line 461
  95. def OAI.MUB6.Certificate.PairSemantics.raw8152step2 line 463
  96. def OAI.MUB6.Certificate.PairSemantics.raw8152step3 line 465
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical8152 line 467
  98. def OAI.MUB6.Certificate.PairSemantics.raw8153 line 490
  99. def OAI.MUB6.Certificate.PairSemantics.raw8153step0 line 492
  100. def OAI.MUB6.Certificate.PairSemantics.raw8153step1 line 494
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8153 line 496
  102. def OAI.MUB6.Certificate.PairSemantics.raw8154 line 510
  103. def OAI.MUB6.Certificate.PairSemantics.raw8154step0 line 512
  104. def OAI.MUB6.Certificate.PairSemantics.raw8154step1 line 514
  105. def OAI.MUB6.Certificate.PairSemantics.raw8154step2 line 516
  106. def OAI.MUB6.Certificate.PairSemantics.raw8154step3 line 518
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8154 line 520
  108. def OAI.MUB6.Certificate.PairSemantics.raw8155 line 543
  109. def OAI.MUB6.Certificate.PairSemantics.raw8155step0 line 545
  110. def OAI.MUB6.Certificate.PairSemantics.raw8155step1 line 547
  111. def OAI.MUB6.Certificate.PairSemantics.raw8155step2 line 549
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical8155 line 551
  113. def OAI.MUB6.Certificate.PairSemantics.raw8156 line 569
  114. def OAI.MUB6.Certificate.PairSemantics.raw8156step0 line 571
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical8156 line 573
  116. def OAI.MUB6.Certificate.PairSemantics.raw8157 line 583
  117. def OAI.MUB6.Certificate.PairSemantics.raw8157step0 line 585
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical8157 line 587
  119. def OAI.MUB6.Certificate.PairSemantics.raw8158 line 597
  120. def OAI.MUB6.Certificate.PairSemantics.raw8158step0 line 599
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical8158 line 601
  122. def OAI.MUB6.Certificate.PairSemantics.raw8159 line 610
  123. def OAI.MUB6.Certificate.PairSemantics.raw8159step0 line 612
  124. def OAI.MUB6.Certificate.PairSemantics.raw8159step1 line 614
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical8159 line 616