OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical39.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1248 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw1248step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw1248step1 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw1248step2 line 25
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1248 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw1249 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw1249step0 line 46
  8. def OAI.MUB6.Certificate.PairSemantics.raw1249step1 line 48
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1249 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw1250 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw1250step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw1250step1 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1250 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw1251 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw1251step0 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw1251step1 line 86
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1251 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw1252 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw1252step0 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw1252step1 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw1252step2 line 107
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1252 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw1253 line 126
  24. def OAI.MUB6.Certificate.PairSemantics.raw1253step0 line 128
  25. def OAI.MUB6.Certificate.PairSemantics.raw1253step1 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw1253step2 line 132
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1253 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw1254 line 151
  29. def OAI.MUB6.Certificate.PairSemantics.raw1254step0 line 153
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1254 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw1255 line 164
  32. def OAI.MUB6.Certificate.PairSemantics.raw1255step0 line 166
  33. def OAI.MUB6.Certificate.PairSemantics.raw1255step1 line 168
  34. def OAI.MUB6.Certificate.PairSemantics.raw1255step2 line 170
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1255 line 172
  36. def OAI.MUB6.Certificate.PairSemantics.raw1256 line 189
  37. def OAI.MUB6.Certificate.PairSemantics.raw1256step0 line 191
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1256 line 193
  39. def OAI.MUB6.Certificate.PairSemantics.raw1257 line 202
  40. def OAI.MUB6.Certificate.PairSemantics.raw1257step0 line 204
  41. def OAI.MUB6.Certificate.PairSemantics.raw1257step1 line 206
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1257 line 208
  43. def OAI.MUB6.Certificate.PairSemantics.raw1258 line 221
  44. def OAI.MUB6.Certificate.PairSemantics.raw1258step0 line 223
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1258 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw1259 line 234
  47. def OAI.MUB6.Certificate.PairSemantics.raw1259step0 line 236
  48. def OAI.MUB6.Certificate.PairSemantics.raw1259step1 line 238
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1259 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw1260 line 253
  51. def OAI.MUB6.Certificate.PairSemantics.raw1260step0 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw1260step1 line 257
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1260 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw1261 line 272
  55. def OAI.MUB6.Certificate.PairSemantics.raw1261step0 line 274
  56. def OAI.MUB6.Certificate.PairSemantics.raw1261step1 line 276
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1261 line 278
  58. def OAI.MUB6.Certificate.PairSemantics.raw1262 line 291
  59. def OAI.MUB6.Certificate.PairSemantics.raw1262step0 line 293
  60. def OAI.MUB6.Certificate.PairSemantics.raw1262step1 line 295
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1262 line 297
  62. def OAI.MUB6.Certificate.PairSemantics.raw1263 line 310
  63. def OAI.MUB6.Certificate.PairSemantics.raw1263step0 line 312
  64. def OAI.MUB6.Certificate.PairSemantics.raw1263step1 line 314
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1263 line 316
  66. def OAI.MUB6.Certificate.PairSemantics.raw1264 line 329
  67. def OAI.MUB6.Certificate.PairSemantics.raw1264step0 line 331
  68. def OAI.MUB6.Certificate.PairSemantics.raw1264step1 line 333
  69. def OAI.MUB6.Certificate.PairSemantics.raw1264step2 line 335
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1264 line 337
  71. def OAI.MUB6.Certificate.PairSemantics.raw1265 line 354
  72. def OAI.MUB6.Certificate.PairSemantics.raw1265step0 line 356
  73. def OAI.MUB6.Certificate.PairSemantics.raw1265step1 line 358
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1265 line 360
  75. def OAI.MUB6.Certificate.PairSemantics.raw1266 line 373
  76. def OAI.MUB6.Certificate.PairSemantics.raw1266step0 line 375
  77. def OAI.MUB6.Certificate.PairSemantics.raw1266step1 line 377
  78. def OAI.MUB6.Certificate.PairSemantics.raw1266step2 line 379
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical1266 line 381
  80. def OAI.MUB6.Certificate.PairSemantics.raw1267 line 398
  81. def OAI.MUB6.Certificate.PairSemantics.raw1267step0 line 400
  82. def OAI.MUB6.Certificate.PairSemantics.raw1267step1 line 402
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1267 line 404
  84. def OAI.MUB6.Certificate.PairSemantics.raw1268 line 417
  85. def OAI.MUB6.Certificate.PairSemantics.raw1268step0 line 419
  86. def OAI.MUB6.Certificate.PairSemantics.raw1268step1 line 421
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1268 line 423
  88. def OAI.MUB6.Certificate.PairSemantics.raw1269 line 436
  89. def OAI.MUB6.Certificate.PairSemantics.raw1269step0 line 438
  90. def OAI.MUB6.Certificate.PairSemantics.raw1269step1 line 440
  91. def OAI.MUB6.Certificate.PairSemantics.raw1269step2 line 442
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1269 line 444
  93. def OAI.MUB6.Certificate.PairSemantics.raw1270 line 461
  94. def OAI.MUB6.Certificate.PairSemantics.raw1270step0 line 463
  95. def OAI.MUB6.Certificate.PairSemantics.raw1270step1 line 465
  96. def OAI.MUB6.Certificate.PairSemantics.raw1270step2 line 467
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical1270 line 469
  98. def OAI.MUB6.Certificate.PairSemantics.raw1271 line 486
  99. def OAI.MUB6.Certificate.PairSemantics.raw1271step0 line 488
  100. def OAI.MUB6.Certificate.PairSemantics.raw1271step1 line 490
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical1271 line 492
  102. def OAI.MUB6.Certificate.PairSemantics.raw1272 line 505
  103. def OAI.MUB6.Certificate.PairSemantics.raw1272step0 line 507
  104. def OAI.MUB6.Certificate.PairSemantics.raw1272step1 line 509
  105. def OAI.MUB6.Certificate.PairSemantics.raw1272step2 line 511
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical1272 line 513
  107. def OAI.MUB6.Certificate.PairSemantics.raw1273 line 530
  108. def OAI.MUB6.Certificate.PairSemantics.raw1273step0 line 532
  109. def OAI.MUB6.Certificate.PairSemantics.raw1273step1 line 534
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical1273 line 536
  111. def OAI.MUB6.Certificate.PairSemantics.raw1274 line 549
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical1274 line 551
  113. def OAI.MUB6.Certificate.PairSemantics.raw1275 line 555
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical1275 line 557
  115. def OAI.MUB6.Certificate.PairSemantics.raw1276 line 561
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical1276 line 563
  117. def OAI.MUB6.Certificate.PairSemantics.raw1277 line 567
  118. def OAI.MUB6.Certificate.PairSemantics.raw1277step0 line 569
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical1277 line 571
  120. def OAI.MUB6.Certificate.PairSemantics.raw1278 line 580
  121. def OAI.MUB6.Certificate.PairSemantics.raw1278step0 line 582
  122. def OAI.MUB6.Certificate.PairSemantics.raw1278step1 line 584
  123. def OAI.MUB6.Certificate.PairSemantics.raw1278step2 line 586
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical1278 line 588
  125. def OAI.MUB6.Certificate.PairSemantics.raw1279 line 605
  126. def OAI.MUB6.Certificate.PairSemantics.raw1279step0 line 607
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical1279 line 609