OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical71.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2272 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw2272step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw2272step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2272 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw2273 line 36
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2273 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw2274 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw2274step0 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2274 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw2275 line 55
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2275 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw2276 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw2276step0 line 63
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical2276 line 65
  15. def OAI.MUB6.Certificate.PairSemantics.raw2277 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw2277step0 line 76
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2277 line 78
  18. def OAI.MUB6.Certificate.PairSemantics.raw2278 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw2278step0 line 89
  20. def OAI.MUB6.Certificate.PairSemantics.raw2278step1 line 91
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2278 line 93
  22. def OAI.MUB6.Certificate.PairSemantics.raw2279 line 106
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2279 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw2280 line 112
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2280 line 114
  26. def OAI.MUB6.Certificate.PairSemantics.raw2281 line 118
  27. def OAI.MUB6.Certificate.PairSemantics.raw2281step0 line 120
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2281 line 122
  29. def OAI.MUB6.Certificate.PairSemantics.raw2282 line 131
  30. def OAI.MUB6.Certificate.PairSemantics.raw2282step0 line 133
  31. def OAI.MUB6.Certificate.PairSemantics.raw2282step1 line 135
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2282 line 137
  33. def OAI.MUB6.Certificate.PairSemantics.raw2283 line 150
  34. def OAI.MUB6.Certificate.PairSemantics.raw2283step0 line 152
  35. def OAI.MUB6.Certificate.PairSemantics.raw2283step1 line 154
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2283 line 156
  37. def OAI.MUB6.Certificate.PairSemantics.raw2284 line 169
  38. def OAI.MUB6.Certificate.PairSemantics.raw2284step0 line 171
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2284 line 173
  40. def OAI.MUB6.Certificate.PairSemantics.raw2285 line 182
  41. def OAI.MUB6.Certificate.PairSemantics.raw2285step0 line 184
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2285 line 186
  43. def OAI.MUB6.Certificate.PairSemantics.raw2286 line 195
  44. def OAI.MUB6.Certificate.PairSemantics.raw2286step0 line 197
  45. def OAI.MUB6.Certificate.PairSemantics.raw2286step1 line 199
  46. def OAI.MUB6.Certificate.PairSemantics.raw2286step2 line 201
  47. def OAI.MUB6.Certificate.PairSemantics.raw2286step3 line 203
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2286 line 205
  49. def OAI.MUB6.Certificate.PairSemantics.raw2287 line 227
  50. def OAI.MUB6.Certificate.PairSemantics.raw2287step0 line 229
  51. def OAI.MUB6.Certificate.PairSemantics.raw2287step1 line 231
  52. def OAI.MUB6.Certificate.PairSemantics.raw2287step2 line 233
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2287 line 235
  54. def OAI.MUB6.Certificate.PairSemantics.raw2288 line 253
  55. def OAI.MUB6.Certificate.PairSemantics.raw2288step0 line 255
  56. def OAI.MUB6.Certificate.PairSemantics.raw2288step1 line 257
  57. def OAI.MUB6.Certificate.PairSemantics.raw2288step2 line 259
  58. def OAI.MUB6.Certificate.PairSemantics.raw2288step3 line 261
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2288 line 263
  60. def OAI.MUB6.Certificate.PairSemantics.raw2289 line 285
  61. def OAI.MUB6.Certificate.PairSemantics.raw2289step0 line 287
  62. def OAI.MUB6.Certificate.PairSemantics.raw2289step1 line 289
  63. def OAI.MUB6.Certificate.PairSemantics.raw2289step2 line 291
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2289 line 293
  65. def OAI.MUB6.Certificate.PairSemantics.raw2290 line 311
  66. def OAI.MUB6.Certificate.PairSemantics.raw2290step0 line 313
  67. def OAI.MUB6.Certificate.PairSemantics.raw2290step1 line 315
  68. def OAI.MUB6.Certificate.PairSemantics.raw2290step2 line 317
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2290 line 319
  70. def OAI.MUB6.Certificate.PairSemantics.raw2291 line 337
  71. def OAI.MUB6.Certificate.PairSemantics.raw2291step0 line 339
  72. def OAI.MUB6.Certificate.PairSemantics.raw2291step1 line 341
  73. def OAI.MUB6.Certificate.PairSemantics.raw2291step2 line 343
  74. def OAI.MUB6.Certificate.PairSemantics.raw2291step3 line 345
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2291 line 347
  76. def OAI.MUB6.Certificate.PairSemantics.raw2292 line 369
  77. def OAI.MUB6.Certificate.PairSemantics.raw2292step0 line 371
  78. def OAI.MUB6.Certificate.PairSemantics.raw2292step1 line 373
  79. def OAI.MUB6.Certificate.PairSemantics.raw2292step2 line 375
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2292 line 377
  81. def OAI.MUB6.Certificate.PairSemantics.raw2293 line 395
  82. def OAI.MUB6.Certificate.PairSemantics.raw2293step0 line 397
  83. def OAI.MUB6.Certificate.PairSemantics.raw2293step1 line 399
  84. def OAI.MUB6.Certificate.PairSemantics.raw2293step2 line 401
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical2293 line 403
  86. def OAI.MUB6.Certificate.PairSemantics.raw2294 line 421
  87. def OAI.MUB6.Certificate.PairSemantics.raw2294step0 line 423
  88. def OAI.MUB6.Certificate.PairSemantics.raw2294step1 line 425
  89. def OAI.MUB6.Certificate.PairSemantics.raw2294step2 line 427
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2294 line 429
  91. def OAI.MUB6.Certificate.PairSemantics.raw2295 line 447
  92. def OAI.MUB6.Certificate.PairSemantics.raw2295step0 line 449
  93. def OAI.MUB6.Certificate.PairSemantics.raw2295step1 line 451
  94. def OAI.MUB6.Certificate.PairSemantics.raw2295step2 line 453
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical2295 line 455
  96. def OAI.MUB6.Certificate.PairSemantics.raw2296 line 473
  97. def OAI.MUB6.Certificate.PairSemantics.raw2296step0 line 475
  98. def OAI.MUB6.Certificate.PairSemantics.raw2296step1 line 477
  99. def OAI.MUB6.Certificate.PairSemantics.raw2296step2 line 479
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical2296 line 481
  101. def OAI.MUB6.Certificate.PairSemantics.raw2297 line 499
  102. def OAI.MUB6.Certificate.PairSemantics.raw2297step0 line 501
  103. def OAI.MUB6.Certificate.PairSemantics.raw2297step1 line 503
  104. def OAI.MUB6.Certificate.PairSemantics.raw2297step2 line 505
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical2297 line 507
  106. def OAI.MUB6.Certificate.PairSemantics.raw2298 line 525
  107. def OAI.MUB6.Certificate.PairSemantics.raw2298step0 line 527
  108. def OAI.MUB6.Certificate.PairSemantics.raw2298step1 line 529
  109. def OAI.MUB6.Certificate.PairSemantics.raw2298step2 line 531
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical2298 line 533
  111. def OAI.MUB6.Certificate.PairSemantics.raw2299 line 551
  112. def OAI.MUB6.Certificate.PairSemantics.raw2299step0 line 553
  113. def OAI.MUB6.Certificate.PairSemantics.raw2299step1 line 555
  114. def OAI.MUB6.Certificate.PairSemantics.raw2299step2 line 557
  115. def OAI.MUB6.Certificate.PairSemantics.raw2299step3 line 559
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical2299 line 561
  117. def OAI.MUB6.Certificate.PairSemantics.raw2300 line 583
  118. def OAI.MUB6.Certificate.PairSemantics.raw2300step0 line 585
  119. def OAI.MUB6.Certificate.PairSemantics.raw2300step1 line 587
  120. def OAI.MUB6.Certificate.PairSemantics.raw2300step2 line 589
  121. def OAI.MUB6.Certificate.PairSemantics.raw2300step3 line 591
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical2300 line 593
  123. def OAI.MUB6.Certificate.PairSemantics.raw2301 line 615
  124. def OAI.MUB6.Certificate.PairSemantics.raw2301step0 line 617
  125. def OAI.MUB6.Certificate.PairSemantics.raw2301step1 line 619
  126. def OAI.MUB6.Certificate.PairSemantics.raw2301step2 line 621
  127. def OAI.MUB6.Certificate.PairSemantics.raw2301step3 line 623
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical2301 line 625
  129. def OAI.MUB6.Certificate.PairSemantics.raw2302 line 647
  130. def OAI.MUB6.Certificate.PairSemantics.raw2302step0 line 649
  131. def OAI.MUB6.Certificate.PairSemantics.raw2302step1 line 651
  132. def OAI.MUB6.Certificate.PairSemantics.raw2302step2 line 653
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical2302 line 655
  134. def OAI.MUB6.Certificate.PairSemantics.raw2303 line 673
  135. def OAI.MUB6.Certificate.PairSemantics.raw2303step0 line 675
  136. def OAI.MUB6.Certificate.PairSemantics.raw2303step1 line 677
  137. def OAI.MUB6.Certificate.PairSemantics.raw2303step2 line 679
  138. def OAI.MUB6.Certificate.PairSemantics.raw2303step3 line 681
  139. theorem OAI.MUB6.Certificate.PairSemantics.canonical2303 line 683