OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical38.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1216 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw1216step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1216step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1216 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw1217 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw1217step0 line 37
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1217 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw1218 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw1218step0 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw1218step1 line 52
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1218 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw1219 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw1219step0 line 69
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1219 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw1220 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw1220step0 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw1220step1 line 84
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1220 line 86
  19. def OAI.MUB6.Certificate.PairSemantics.raw1221 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw1221step0 line 101
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1221 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw1222 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw1222step0 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw1222step1 line 116
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1222 line 118
  26. def OAI.MUB6.Certificate.PairSemantics.raw1223 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw1223step0 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw1223step1 line 135
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1223 line 137
  30. def OAI.MUB6.Certificate.PairSemantics.raw1224 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw1224step0 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw1224step1 line 154
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1224 line 156
  34. def OAI.MUB6.Certificate.PairSemantics.raw1225 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw1225step0 line 171
  36. def OAI.MUB6.Certificate.PairSemantics.raw1225step1 line 173
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1225 line 175
  38. def OAI.MUB6.Certificate.PairSemantics.raw1226 line 188
  39. def OAI.MUB6.Certificate.PairSemantics.raw1226step0 line 190
  40. def OAI.MUB6.Certificate.PairSemantics.raw1226step1 line 192
  41. def OAI.MUB6.Certificate.PairSemantics.raw1226step2 line 194
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1226 line 196
  43. def OAI.MUB6.Certificate.PairSemantics.raw1227 line 213
  44. def OAI.MUB6.Certificate.PairSemantics.raw1227step0 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw1227step1 line 217
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1227 line 219
  47. def OAI.MUB6.Certificate.PairSemantics.raw1228 line 232
  48. def OAI.MUB6.Certificate.PairSemantics.raw1228step0 line 234
  49. def OAI.MUB6.Certificate.PairSemantics.raw1228step1 line 236
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1228 line 238
  51. def OAI.MUB6.Certificate.PairSemantics.raw1229 line 251
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical1229 line 253
  53. def OAI.MUB6.Certificate.PairSemantics.raw1230 line 257
  54. def OAI.MUB6.Certificate.PairSemantics.raw1230step0 line 259
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1230 line 261
  56. def OAI.MUB6.Certificate.PairSemantics.raw1231 line 270
  57. def OAI.MUB6.Certificate.PairSemantics.raw1231step0 line 272
  58. def OAI.MUB6.Certificate.PairSemantics.raw1231step1 line 274
  59. def OAI.MUB6.Certificate.PairSemantics.raw1231step2 line 276
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1231 line 278
  61. def OAI.MUB6.Certificate.PairSemantics.raw1232 line 295
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1232 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw1233 line 301
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical1233 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw1234 line 307
  66. def OAI.MUB6.Certificate.PairSemantics.raw1234step0 line 309
  67. def OAI.MUB6.Certificate.PairSemantics.raw1234step1 line 311
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1234 line 313
  69. def OAI.MUB6.Certificate.PairSemantics.raw1235 line 326
  70. def OAI.MUB6.Certificate.PairSemantics.raw1235step0 line 328
  71. def OAI.MUB6.Certificate.PairSemantics.raw1235step1 line 330
  72. def OAI.MUB6.Certificate.PairSemantics.raw1235step2 line 332
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1235 line 334
  74. def OAI.MUB6.Certificate.PairSemantics.raw1236 line 351
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1236 line 353
  76. def OAI.MUB6.Certificate.PairSemantics.raw1237 line 357
  77. def OAI.MUB6.Certificate.PairSemantics.raw1237step0 line 359
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1237 line 361
  79. def OAI.MUB6.Certificate.PairSemantics.raw1238 line 370
  80. def OAI.MUB6.Certificate.PairSemantics.raw1238step0 line 372
  81. def OAI.MUB6.Certificate.PairSemantics.raw1238step1 line 374
  82. def OAI.MUB6.Certificate.PairSemantics.raw1238step2 line 376
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1238 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw1239 line 395
  85. def OAI.MUB6.Certificate.PairSemantics.raw1239step0 line 397
  86. def OAI.MUB6.Certificate.PairSemantics.raw1239step1 line 399
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1239 line 401
  88. def OAI.MUB6.Certificate.PairSemantics.raw1240 line 414
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1240 line 416
  90. def OAI.MUB6.Certificate.PairSemantics.raw1241 line 420
  91. def OAI.MUB6.Certificate.PairSemantics.raw1241step0 line 422
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1241 line 424
  93. def OAI.MUB6.Certificate.PairSemantics.raw1242 line 433
  94. def OAI.MUB6.Certificate.PairSemantics.raw1242step0 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw1242step1 line 437
  96. def OAI.MUB6.Certificate.PairSemantics.raw1242step2 line 439
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical1242 line 441
  98. def OAI.MUB6.Certificate.PairSemantics.raw1243 line 458
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical1243 line 460
  100. def OAI.MUB6.Certificate.PairSemantics.raw1244 line 464
  101. def OAI.MUB6.Certificate.PairSemantics.raw1244step0 line 466
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical1244 line 468
  103. def OAI.MUB6.Certificate.PairSemantics.raw1245 line 477
  104. def OAI.MUB6.Certificate.PairSemantics.raw1245step0 line 479
  105. def OAI.MUB6.Certificate.PairSemantics.raw1245step1 line 481
  106. def OAI.MUB6.Certificate.PairSemantics.raw1245step2 line 483
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical1245 line 485
  108. def OAI.MUB6.Certificate.PairSemantics.raw1246 line 502
  109. def OAI.MUB6.Certificate.PairSemantics.raw1246step0 line 504
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical1246 line 506
  111. def OAI.MUB6.Certificate.PairSemantics.raw1247 line 515
  112. def OAI.MUB6.Certificate.PairSemantics.raw1247step0 line 517
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical1247 line 519