OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical40.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1280 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1280 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw1281 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw1281step0 line 21
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1281 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw1282 line 32
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1282 line 34
  8. def OAI.MUB6.Certificate.PairSemantics.raw1283 line 38
  9. def OAI.MUB6.Certificate.PairSemantics.raw1283step0 line 40
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1283 line 42
  11. def OAI.MUB6.Certificate.PairSemantics.raw1284 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw1284step0 line 53
  13. def OAI.MUB6.Certificate.PairSemantics.raw1284step1 line 55
  14. def OAI.MUB6.Certificate.PairSemantics.raw1284step2 line 57
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1284 line 59
  16. def OAI.MUB6.Certificate.PairSemantics.raw1285 line 76
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1285 line 78
  18. def OAI.MUB6.Certificate.PairSemantics.raw1286 line 82
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1286 line 84
  20. def OAI.MUB6.Certificate.PairSemantics.raw1287 line 88
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1287 line 90
  22. def OAI.MUB6.Certificate.PairSemantics.raw1288 line 94
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1288 line 96
  24. def OAI.MUB6.Certificate.PairSemantics.raw1289 line 100
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1289 line 102
  26. def OAI.MUB6.Certificate.PairSemantics.raw1290 line 106
  27. def OAI.MUB6.Certificate.PairSemantics.raw1290step0 line 108
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1290 line 110
  29. def OAI.MUB6.Certificate.PairSemantics.raw1291 line 119
  30. def OAI.MUB6.Certificate.PairSemantics.raw1291step0 line 121
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical1291 line 123
  32. def OAI.MUB6.Certificate.PairSemantics.raw1292 line 132
  33. def OAI.MUB6.Certificate.PairSemantics.raw1292step0 line 134
  34. def OAI.MUB6.Certificate.PairSemantics.raw1292step1 line 136
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1292 line 138
  36. def OAI.MUB6.Certificate.PairSemantics.raw1293 line 151
  37. def OAI.MUB6.Certificate.PairSemantics.raw1293step0 line 153
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1293 line 155
  39. def OAI.MUB6.Certificate.PairSemantics.raw1294 line 164
  40. def OAI.MUB6.Certificate.PairSemantics.raw1294step0 line 166
  41. def OAI.MUB6.Certificate.PairSemantics.raw1294step1 line 168
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1294 line 170
  43. def OAI.MUB6.Certificate.PairSemantics.raw1295 line 183
  44. def OAI.MUB6.Certificate.PairSemantics.raw1295step0 line 185
  45. def OAI.MUB6.Certificate.PairSemantics.raw1295step1 line 187
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1295 line 189
  47. def OAI.MUB6.Certificate.PairSemantics.raw1296 line 202
  48. def OAI.MUB6.Certificate.PairSemantics.raw1296step0 line 204
  49. def OAI.MUB6.Certificate.PairSemantics.raw1296step1 line 206
  50. def OAI.MUB6.Certificate.PairSemantics.raw1296step2 line 208
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1296 line 210
  52. def OAI.MUB6.Certificate.PairSemantics.raw1297 line 228
  53. def OAI.MUB6.Certificate.PairSemantics.raw1297step0 line 230
  54. def OAI.MUB6.Certificate.PairSemantics.raw1297step1 line 232
  55. def OAI.MUB6.Certificate.PairSemantics.raw1297step2 line 234
  56. def OAI.MUB6.Certificate.PairSemantics.raw1297step3 line 236
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1297 line 238
  58. def OAI.MUB6.Certificate.PairSemantics.raw1298 line 260
  59. def OAI.MUB6.Certificate.PairSemantics.raw1298step0 line 262
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1298 line 264
  61. def OAI.MUB6.Certificate.PairSemantics.raw1299 line 273
  62. def OAI.MUB6.Certificate.PairSemantics.raw1299step0 line 275
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1299 line 277
  64. def OAI.MUB6.Certificate.PairSemantics.raw1300 line 286
  65. def OAI.MUB6.Certificate.PairSemantics.raw1300step0 line 288
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1300 line 290
  67. def OAI.MUB6.Certificate.PairSemantics.raw1301 line 299
  68. def OAI.MUB6.Certificate.PairSemantics.raw1301step0 line 301
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1301 line 303
  70. def OAI.MUB6.Certificate.PairSemantics.raw1302 line 312
  71. def OAI.MUB6.Certificate.PairSemantics.raw1302step0 line 314
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1302 line 316
  73. def OAI.MUB6.Certificate.PairSemantics.raw1303 line 325
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1303 line 327
  75. def OAI.MUB6.Certificate.PairSemantics.raw1304 line 331
  76. def OAI.MUB6.Certificate.PairSemantics.raw1304step0 line 333
  77. def OAI.MUB6.Certificate.PairSemantics.raw1304step1 line 335
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1304 line 337
  79. def OAI.MUB6.Certificate.PairSemantics.raw1305 line 350
  80. def OAI.MUB6.Certificate.PairSemantics.raw1305step0 line 352
  81. def OAI.MUB6.Certificate.PairSemantics.raw1305step1 line 354
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1305 line 356
  83. def OAI.MUB6.Certificate.PairSemantics.raw1306 line 369
  84. def OAI.MUB6.Certificate.PairSemantics.raw1306step0 line 371
  85. def OAI.MUB6.Certificate.PairSemantics.raw1306step1 line 373
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1306 line 375
  87. def OAI.MUB6.Certificate.PairSemantics.raw1307 line 388
  88. def OAI.MUB6.Certificate.PairSemantics.raw1307step0 line 390
  89. def OAI.MUB6.Certificate.PairSemantics.raw1307step1 line 392
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1307 line 394
  91. def OAI.MUB6.Certificate.PairSemantics.raw1308 line 407
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1308 line 409
  93. def OAI.MUB6.Certificate.PairSemantics.raw1309 line 413
  94. def OAI.MUB6.Certificate.PairSemantics.raw1309step0 line 415
  95. def OAI.MUB6.Certificate.PairSemantics.raw1309step1 line 417
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1309 line 419
  97. def OAI.MUB6.Certificate.PairSemantics.raw1310 line 432
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical1310 line 434
  99. def OAI.MUB6.Certificate.PairSemantics.raw1311 line 438
  100. def OAI.MUB6.Certificate.PairSemantics.raw1311step0 line 440
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical1311 line 442