OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical102.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3264 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw3264step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical3264 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw3265 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw3265step0 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw3265step1 line 36
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3265 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw3266 line 51
  9. def OAI.MUB6.Certificate.PairSemantics.raw3266step0 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw3266step1 line 55
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3266 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw3267 line 70
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3267 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw3268 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw3268step0 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw3268step1 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw3268step2 line 82
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3268 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw3269 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw3269step0 line 103
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3269 line 105
  22. def OAI.MUB6.Certificate.PairSemantics.raw3270 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw3270step0 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw3270step1 line 118
  25. def OAI.MUB6.Certificate.PairSemantics.raw3270step2 line 120
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3270 line 122
  27. def OAI.MUB6.Certificate.PairSemantics.raw3271 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw3271step0 line 141
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical3271 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw3272 line 152
  31. def OAI.MUB6.Certificate.PairSemantics.raw3272step0 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw3272step1 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw3272step2 line 158
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical3272 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw3273 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw3273step0 line 179
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3273 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw3274 line 190
  39. def OAI.MUB6.Certificate.PairSemantics.raw3274step0 line 192
  40. def OAI.MUB6.Certificate.PairSemantics.raw3274step1 line 194
  41. def OAI.MUB6.Certificate.PairSemantics.raw3274step2 line 196
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3274 line 198
  43. def OAI.MUB6.Certificate.PairSemantics.raw3275 line 215
  44. def OAI.MUB6.Certificate.PairSemantics.raw3275step0 line 217
  45. def OAI.MUB6.Certificate.PairSemantics.raw3275step1 line 219
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3275 line 221
  47. def OAI.MUB6.Certificate.PairSemantics.raw3276 line 234
  48. def OAI.MUB6.Certificate.PairSemantics.raw3276step0 line 236
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3276 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw3277 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw3277step0 line 249
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3277 line 251
  53. def OAI.MUB6.Certificate.PairSemantics.raw3278 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw3278step0 line 262
  55. def OAI.MUB6.Certificate.PairSemantics.raw3278step1 line 264
  56. def OAI.MUB6.Certificate.PairSemantics.raw3278step2 line 266
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3278 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw3279 line 285
  59. def OAI.MUB6.Certificate.PairSemantics.raw3279step0 line 287
  60. def OAI.MUB6.Certificate.PairSemantics.raw3279step1 line 289
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3279 line 291
  62. def OAI.MUB6.Certificate.PairSemantics.raw3280 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw3280step0 line 306
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical3280 line 308
  65. def OAI.MUB6.Certificate.PairSemantics.raw3281 line 317
  66. def OAI.MUB6.Certificate.PairSemantics.raw3281step0 line 319
  67. def OAI.MUB6.Certificate.PairSemantics.raw3281step1 line 321
  68. def OAI.MUB6.Certificate.PairSemantics.raw3281step2 line 323
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3281 line 325
  70. def OAI.MUB6.Certificate.PairSemantics.raw3282 line 342
  71. def OAI.MUB6.Certificate.PairSemantics.raw3282step0 line 344
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3282 line 346
  73. def OAI.MUB6.Certificate.PairSemantics.raw3283 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw3283step0 line 357
  75. def OAI.MUB6.Certificate.PairSemantics.raw3283step1 line 359
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical3283 line 361
  77. def OAI.MUB6.Certificate.PairSemantics.raw3284 line 374
  78. def OAI.MUB6.Certificate.PairSemantics.raw3284step0 line 376
  79. def OAI.MUB6.Certificate.PairSemantics.raw3284step1 line 378
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3284 line 380
  81. def OAI.MUB6.Certificate.PairSemantics.raw3285 line 393
  82. def OAI.MUB6.Certificate.PairSemantics.raw3285step0 line 395
  83. def OAI.MUB6.Certificate.PairSemantics.raw3285step1 line 397
  84. def OAI.MUB6.Certificate.PairSemantics.raw3285step2 line 399
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3285 line 401
  86. def OAI.MUB6.Certificate.PairSemantics.raw3286 line 418
  87. def OAI.MUB6.Certificate.PairSemantics.raw3286step0 line 420
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical3286 line 422
  89. def OAI.MUB6.Certificate.PairSemantics.raw3287 line 431
  90. def OAI.MUB6.Certificate.PairSemantics.raw3287step0 line 433
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical3287 line 435
  92. def OAI.MUB6.Certificate.PairSemantics.raw3288 line 444
  93. def OAI.MUB6.Certificate.PairSemantics.raw3288step0 line 446
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3288 line 448
  95. def OAI.MUB6.Certificate.PairSemantics.raw3289 line 457
  96. def OAI.MUB6.Certificate.PairSemantics.raw3289step0 line 459
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical3289 line 461
  98. def OAI.MUB6.Certificate.PairSemantics.raw3290 line 470
  99. def OAI.MUB6.Certificate.PairSemantics.raw3290step0 line 472
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3290 line 474
  101. def OAI.MUB6.Certificate.PairSemantics.raw3291 line 483
  102. def OAI.MUB6.Certificate.PairSemantics.raw3291step0 line 485
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3291 line 487
  104. def OAI.MUB6.Certificate.PairSemantics.raw3292 line 496
  105. def OAI.MUB6.Certificate.PairSemantics.raw3292step0 line 498
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical3292 line 500
  107. def OAI.MUB6.Certificate.PairSemantics.raw3293 line 509
  108. def OAI.MUB6.Certificate.PairSemantics.raw3293step0 line 511
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical3293 line 513
  110. def OAI.MUB6.Certificate.PairSemantics.raw3294 line 522
  111. def OAI.MUB6.Certificate.PairSemantics.raw3294step0 line 524
  112. def OAI.MUB6.Certificate.PairSemantics.raw3294step1 line 526
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical3294 line 528
  114. def OAI.MUB6.Certificate.PairSemantics.raw3295 line 541
  115. def OAI.MUB6.Certificate.PairSemantics.raw3295step0 line 543
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical3295 line 545