OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical101.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3232 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw3232step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw3232step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3232 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw3233 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw3233step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw3233step1 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw3233step2 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3233 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw3234 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw3234step0 line 65
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3234 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw3235 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw3235step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw3235step1 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3235 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw3236 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw3236step0 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw3236step1 line 99
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3236 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw3237 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw3237step0 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw3237step1 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3237 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw3238 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw3238step0 line 135
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3238 line 137
  28. def OAI.MUB6.Certificate.PairSemantics.raw3239 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw3239step0 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw3239step1 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw3239step2 line 152
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3239 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw3240 line 171
  34. def OAI.MUB6.Certificate.PairSemantics.raw3240step0 line 173
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3240 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw3241 line 184
  37. def OAI.MUB6.Certificate.PairSemantics.raw3241step0 line 186
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical3241 line 188
  39. def OAI.MUB6.Certificate.PairSemantics.raw3242 line 197
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3242 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw3243 line 203
  42. def OAI.MUB6.Certificate.PairSemantics.raw3243step0 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw3243step1 line 207
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical3243 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw3244 line 222
  46. def OAI.MUB6.Certificate.PairSemantics.raw3244step0 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw3244step1 line 226
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3244 line 228
  49. def OAI.MUB6.Certificate.PairSemantics.raw3245 line 241
  50. def OAI.MUB6.Certificate.PairSemantics.raw3245step0 line 243
  51. def OAI.MUB6.Certificate.PairSemantics.raw3245step1 line 245
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3245 line 247
  53. def OAI.MUB6.Certificate.PairSemantics.raw3246 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw3246step0 line 262
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3246 line 264
  56. def OAI.MUB6.Certificate.PairSemantics.raw3247 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw3247step0 line 275
  58. def OAI.MUB6.Certificate.PairSemantics.raw3247step1 line 277
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3247 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw3248 line 292
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3248 line 294
  62. def OAI.MUB6.Certificate.PairSemantics.raw3249 line 298
  63. def OAI.MUB6.Certificate.PairSemantics.raw3249step0 line 300
  64. def OAI.MUB6.Certificate.PairSemantics.raw3249step1 line 302
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3249 line 304
  66. def OAI.MUB6.Certificate.PairSemantics.raw3250 line 317
  67. def OAI.MUB6.Certificate.PairSemantics.raw3250step0 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw3250step1 line 321
  69. def OAI.MUB6.Certificate.PairSemantics.raw3250step2 line 323
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3250 line 325
  71. def OAI.MUB6.Certificate.PairSemantics.raw3251 line 342
  72. def OAI.MUB6.Certificate.PairSemantics.raw3251step0 line 344
  73. def OAI.MUB6.Certificate.PairSemantics.raw3251step1 line 346
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical3251 line 348
  75. def OAI.MUB6.Certificate.PairSemantics.raw3252 line 361
  76. def OAI.MUB6.Certificate.PairSemantics.raw3252step0 line 363
  77. def OAI.MUB6.Certificate.PairSemantics.raw3252step1 line 365
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical3252 line 367
  79. def OAI.MUB6.Certificate.PairSemantics.raw3253 line 380
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3253 line 382
  81. def OAI.MUB6.Certificate.PairSemantics.raw3254 line 386
  82. def OAI.MUB6.Certificate.PairSemantics.raw3254step0 line 388
  83. def OAI.MUB6.Certificate.PairSemantics.raw3254step1 line 390
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3254 line 392
  85. def OAI.MUB6.Certificate.PairSemantics.raw3255 line 405
  86. def OAI.MUB6.Certificate.PairSemantics.raw3255step0 line 407
  87. def OAI.MUB6.Certificate.PairSemantics.raw3255step1 line 409
  88. def OAI.MUB6.Certificate.PairSemantics.raw3255step2 line 411
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3255 line 413
  90. def OAI.MUB6.Certificate.PairSemantics.raw3256 line 430
  91. def OAI.MUB6.Certificate.PairSemantics.raw3256step0 line 432
  92. def OAI.MUB6.Certificate.PairSemantics.raw3256step1 line 434
  93. def OAI.MUB6.Certificate.PairSemantics.raw3256step2 line 436
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3256 line 438
  95. def OAI.MUB6.Certificate.PairSemantics.raw3257 line 455
  96. def OAI.MUB6.Certificate.PairSemantics.raw3257step0 line 457
  97. def OAI.MUB6.Certificate.PairSemantics.raw3257step1 line 459
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3257 line 461
  99. def OAI.MUB6.Certificate.PairSemantics.raw3258 line 474
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3258 line 476
  101. def OAI.MUB6.Certificate.PairSemantics.raw3259 line 480
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3259 line 482
  103. def OAI.MUB6.Certificate.PairSemantics.raw3260 line 486
  104. def OAI.MUB6.Certificate.PairSemantics.raw3260step0 line 488
  105. def OAI.MUB6.Certificate.PairSemantics.raw3260step1 line 490
  106. def OAI.MUB6.Certificate.PairSemantics.raw3260step2 line 492
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3260 line 494
  108. def OAI.MUB6.Certificate.PairSemantics.raw3261 line 511
  109. def OAI.MUB6.Certificate.PairSemantics.raw3261step0 line 513
  110. def OAI.MUB6.Certificate.PairSemantics.raw3261step1 line 515
  111. def OAI.MUB6.Certificate.PairSemantics.raw3261step2 line 517
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical3261 line 519
  113. def OAI.MUB6.Certificate.PairSemantics.raw3262 line 536
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical3262 line 538
  115. def OAI.MUB6.Certificate.PairSemantics.raw3263 line 542
  116. def OAI.MUB6.Certificate.PairSemantics.raw3263step0 line 544
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical3263 line 546