OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical293.lean

GitHub source file

135 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9376 line 24
  2. def OAI.MUB6.Certificate.PairSemantics.raw9376step0 line 26
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9376 line 28
  4. def OAI.MUB6.Certificate.PairSemantics.raw9377 line 37
  5. def OAI.MUB6.Certificate.PairSemantics.raw9377step0 line 39
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9377 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw9378 line 50
  8. def OAI.MUB6.Certificate.PairSemantics.raw9378step0 line 52
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9378 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw9379 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw9379step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw9379step1 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9379 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw9380 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw9380step0 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw9380step1 line 86
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical9380 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw9381 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw9381step0 line 103
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical9381 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw9382 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw9382step0 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw9382step1 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical9382 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw9383 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw9383step0 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw9383step1 line 137
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9383 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw9384 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw9384step0 line 154
  31. def OAI.MUB6.Certificate.PairSemantics.raw9384step1 line 156
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical9384 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw9385 line 171
  34. def OAI.MUB6.Certificate.PairSemantics.raw9385step0 line 173
  35. def OAI.MUB6.Certificate.PairSemantics.raw9385step1 line 175
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical9385 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw9386 line 191
  38. def OAI.MUB6.Certificate.PairSemantics.raw9386step0 line 193
  39. def OAI.MUB6.Certificate.PairSemantics.raw9386step1 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw9386step2 line 197
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9386 line 199
  42. def OAI.MUB6.Certificate.PairSemantics.raw9387 line 217
  43. def OAI.MUB6.Certificate.PairSemantics.raw9387step0 line 219
  44. def OAI.MUB6.Certificate.PairSemantics.raw9387step1 line 221
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9387 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw9388 line 237
  47. def OAI.MUB6.Certificate.PairSemantics.raw9388step0 line 239
  48. def OAI.MUB6.Certificate.PairSemantics.raw9388step1 line 241
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical9388 line 243
  50. def OAI.MUB6.Certificate.PairSemantics.raw9389 line 257
  51. def OAI.MUB6.Certificate.PairSemantics.raw9389step0 line 259
  52. def OAI.MUB6.Certificate.PairSemantics.raw9389step1 line 261
  53. def OAI.MUB6.Certificate.PairSemantics.raw9389step2 line 263
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9389 line 265
  55. def OAI.MUB6.Certificate.PairSemantics.raw9390 line 283
  56. def OAI.MUB6.Certificate.PairSemantics.raw9390step0 line 285
  57. def OAI.MUB6.Certificate.PairSemantics.raw9390step1 line 287
  58. def OAI.MUB6.Certificate.PairSemantics.raw9390step2 line 289
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9390 line 291
  60. def OAI.MUB6.Certificate.PairSemantics.raw9391 line 309
  61. def OAI.MUB6.Certificate.PairSemantics.raw9391step0 line 311
  62. def OAI.MUB6.Certificate.PairSemantics.raw9391step1 line 313
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9391 line 315
  64. def OAI.MUB6.Certificate.PairSemantics.raw9392 line 329
  65. def OAI.MUB6.Certificate.PairSemantics.raw9392step0 line 331
  66. def OAI.MUB6.Certificate.PairSemantics.raw9392step1 line 333
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9392 line 335
  68. def OAI.MUB6.Certificate.PairSemantics.raw9393 line 349
  69. def OAI.MUB6.Certificate.PairSemantics.raw9393step0 line 351
  70. def OAI.MUB6.Certificate.PairSemantics.raw9393step1 line 353
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9393 line 355
  72. def OAI.MUB6.Certificate.PairSemantics.raw9394 line 369
  73. def OAI.MUB6.Certificate.PairSemantics.raw9394step0 line 371
  74. def OAI.MUB6.Certificate.PairSemantics.raw9394step1 line 373
  75. def OAI.MUB6.Certificate.PairSemantics.raw9394step2 line 375
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical9394 line 377
  77. def OAI.MUB6.Certificate.PairSemantics.raw9395 line 395
  78. def OAI.MUB6.Certificate.PairSemantics.raw9395step0 line 397
  79. def OAI.MUB6.Certificate.PairSemantics.raw9395step1 line 399
  80. def OAI.MUB6.Certificate.PairSemantics.raw9395step2 line 401
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9395 line 403
  82. def OAI.MUB6.Certificate.PairSemantics.raw9396 line 421
  83. def OAI.MUB6.Certificate.PairSemantics.raw9396step0 line 423
  84. def OAI.MUB6.Certificate.PairSemantics.raw9396step1 line 425
  85. def OAI.MUB6.Certificate.PairSemantics.raw9396step2 line 427
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9396 line 429
  87. def OAI.MUB6.Certificate.PairSemantics.raw9397 line 447
  88. def OAI.MUB6.Certificate.PairSemantics.raw9397step0 line 449
  89. def OAI.MUB6.Certificate.PairSemantics.raw9397step1 line 451
  90. def OAI.MUB6.Certificate.PairSemantics.raw9397step2 line 453
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9397 line 455
  92. def OAI.MUB6.Certificate.PairSemantics.raw9398 line 473
  93. def OAI.MUB6.Certificate.PairSemantics.raw9398step0 line 475
  94. def OAI.MUB6.Certificate.PairSemantics.raw9398step1 line 477
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9398 line 479
  96. def OAI.MUB6.Certificate.PairSemantics.raw9399 line 493
  97. def OAI.MUB6.Certificate.PairSemantics.raw9399step0 line 495
  98. def OAI.MUB6.Certificate.PairSemantics.raw9399step1 line 497
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9399 line 499
  100. def OAI.MUB6.Certificate.PairSemantics.raw9400 line 513
  101. def OAI.MUB6.Certificate.PairSemantics.raw9400step0 line 515
  102. def OAI.MUB6.Certificate.PairSemantics.raw9400step1 line 517
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical9400 line 519
  104. def OAI.MUB6.Certificate.PairSemantics.raw9401 line 533
  105. def OAI.MUB6.Certificate.PairSemantics.raw9401step0 line 535
  106. def OAI.MUB6.Certificate.PairSemantics.raw9401step1 line 537
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9401 line 539
  108. def OAI.MUB6.Certificate.PairSemantics.raw9402 line 553
  109. def OAI.MUB6.Certificate.PairSemantics.raw9402step0 line 555
  110. def OAI.MUB6.Certificate.PairSemantics.raw9402step1 line 557
  111. def OAI.MUB6.Certificate.PairSemantics.raw9402step2 line 559
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical9402 line 561
  113. def OAI.MUB6.Certificate.PairSemantics.raw9403 line 579
  114. def OAI.MUB6.Certificate.PairSemantics.raw9403step0 line 581
  115. def OAI.MUB6.Certificate.PairSemantics.raw9403step1 line 583
  116. def OAI.MUB6.Certificate.PairSemantics.raw9403step2 line 585
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical9403 line 587
  118. def OAI.MUB6.Certificate.PairSemantics.raw9404 line 605
  119. def OAI.MUB6.Certificate.PairSemantics.raw9404step0 line 607
  120. def OAI.MUB6.Certificate.PairSemantics.raw9404step1 line 609
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical9404 line 611
  122. def OAI.MUB6.Certificate.PairSemantics.raw9405 line 625
  123. def OAI.MUB6.Certificate.PairSemantics.raw9405step0 line 627
  124. def OAI.MUB6.Certificate.PairSemantics.raw9405step1 line 629
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical9405 line 631
  126. def OAI.MUB6.Certificate.PairSemantics.raw9406 line 645
  127. def OAI.MUB6.Certificate.PairSemantics.raw9406step0 line 647
  128. def OAI.MUB6.Certificate.PairSemantics.raw9406step1 line 649
  129. def OAI.MUB6.Certificate.PairSemantics.raw9406step2 line 651
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical9406 line 653
  131. def OAI.MUB6.Certificate.PairSemantics.raw9407 line 671
  132. def OAI.MUB6.Certificate.PairSemantics.raw9407step0 line 673
  133. def OAI.MUB6.Certificate.PairSemantics.raw9407step1 line 675
  134. def OAI.MUB6.Certificate.PairSemantics.raw9407step2 line 677
  135. theorem OAI.MUB6.Certificate.PairSemantics.canonical9407 line 679