OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical265.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8480 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw8480step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw8480step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8480 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw8481 line 42
  6. def OAI.MUB6.Certificate.PairSemantics.raw8481step0 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw8481step1 line 46
  8. def OAI.MUB6.Certificate.PairSemantics.raw8481step2 line 48
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8481 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw8482 line 68
  11. def OAI.MUB6.Certificate.PairSemantics.raw8482step0 line 70
  12. def OAI.MUB6.Certificate.PairSemantics.raw8482step1 line 72
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical8482 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw8483 line 88
  15. def OAI.MUB6.Certificate.PairSemantics.raw8483step0 line 90
  16. def OAI.MUB6.Certificate.PairSemantics.raw8483step1 line 92
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8483 line 94
  18. def OAI.MUB6.Certificate.PairSemantics.raw8484 line 108
  19. def OAI.MUB6.Certificate.PairSemantics.raw8484step0 line 110
  20. def OAI.MUB6.Certificate.PairSemantics.raw8484step1 line 112
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical8484 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw8485 line 127
  23. def OAI.MUB6.Certificate.PairSemantics.raw8485step0 line 129
  24. def OAI.MUB6.Certificate.PairSemantics.raw8485step1 line 131
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8485 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw8486 line 146
  27. def OAI.MUB6.Certificate.PairSemantics.raw8486step0 line 148
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8486 line 150
  29. def OAI.MUB6.Certificate.PairSemantics.raw8487 line 159
  30. def OAI.MUB6.Certificate.PairSemantics.raw8487step0 line 161
  31. def OAI.MUB6.Certificate.PairSemantics.raw8487step1 line 163
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical8487 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw8488 line 178
  34. def OAI.MUB6.Certificate.PairSemantics.raw8488step0 line 180
  35. def OAI.MUB6.Certificate.PairSemantics.raw8488step1 line 182
  36. def OAI.MUB6.Certificate.PairSemantics.raw8488step2 line 184
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical8488 line 186
  38. def OAI.MUB6.Certificate.PairSemantics.raw8489 line 203
  39. def OAI.MUB6.Certificate.PairSemantics.raw8489step0 line 205
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8489 line 207
  41. def OAI.MUB6.Certificate.PairSemantics.raw8490 line 216
  42. def OAI.MUB6.Certificate.PairSemantics.raw8490step0 line 218
  43. def OAI.MUB6.Certificate.PairSemantics.raw8490step1 line 220
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8490 line 222
  45. def OAI.MUB6.Certificate.PairSemantics.raw8491 line 235
  46. def OAI.MUB6.Certificate.PairSemantics.raw8491step0 line 237
  47. def OAI.MUB6.Certificate.PairSemantics.raw8491step1 line 239
  48. def OAI.MUB6.Certificate.PairSemantics.raw8491step2 line 241
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8491 line 243
  50. def OAI.MUB6.Certificate.PairSemantics.raw8492 line 261
  51. def OAI.MUB6.Certificate.PairSemantics.raw8492step0 line 263
  52. def OAI.MUB6.Certificate.PairSemantics.raw8492step1 line 265
  53. def OAI.MUB6.Certificate.PairSemantics.raw8492step2 line 267
  54. def OAI.MUB6.Certificate.PairSemantics.raw8492step3 line 269
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8492 line 271
  56. def OAI.MUB6.Certificate.PairSemantics.raw8493 line 294
  57. def OAI.MUB6.Certificate.PairSemantics.raw8493step0 line 296
  58. def OAI.MUB6.Certificate.PairSemantics.raw8493step1 line 298
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8493 line 300
  60. def OAI.MUB6.Certificate.PairSemantics.raw8494 line 314
  61. def OAI.MUB6.Certificate.PairSemantics.raw8494step0 line 316
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8494 line 318
  63. def OAI.MUB6.Certificate.PairSemantics.raw8495 line 327
  64. def OAI.MUB6.Certificate.PairSemantics.raw8495step0 line 329
  65. def OAI.MUB6.Certificate.PairSemantics.raw8495step1 line 331
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8495 line 333
  67. def OAI.MUB6.Certificate.PairSemantics.raw8496 line 347
  68. def OAI.MUB6.Certificate.PairSemantics.raw8496step0 line 349
  69. def OAI.MUB6.Certificate.PairSemantics.raw8496step1 line 351
  70. def OAI.MUB6.Certificate.PairSemantics.raw8496step2 line 353
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8496 line 355
  72. def OAI.MUB6.Certificate.PairSemantics.raw8497 line 373
  73. def OAI.MUB6.Certificate.PairSemantics.raw8497step0 line 375
  74. def OAI.MUB6.Certificate.PairSemantics.raw8497step1 line 377
  75. def OAI.MUB6.Certificate.PairSemantics.raw8497step2 line 379
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8497 line 381
  77. def OAI.MUB6.Certificate.PairSemantics.raw8498 line 399
  78. def OAI.MUB6.Certificate.PairSemantics.raw8498step0 line 401
  79. def OAI.MUB6.Certificate.PairSemantics.raw8498step1 line 403
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical8498 line 405
  81. def OAI.MUB6.Certificate.PairSemantics.raw8499 line 419
  82. def OAI.MUB6.Certificate.PairSemantics.raw8499step0 line 421
  83. def OAI.MUB6.Certificate.PairSemantics.raw8499step1 line 423
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical8499 line 425
  85. def OAI.MUB6.Certificate.PairSemantics.raw8500 line 438
  86. def OAI.MUB6.Certificate.PairSemantics.raw8500step0 line 440
  87. def OAI.MUB6.Certificate.PairSemantics.raw8500step1 line 442
  88. def OAI.MUB6.Certificate.PairSemantics.raw8500step2 line 444
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8500 line 446
  90. def OAI.MUB6.Certificate.PairSemantics.raw8501 line 463
  91. def OAI.MUB6.Certificate.PairSemantics.raw8501step0 line 465
  92. def OAI.MUB6.Certificate.PairSemantics.raw8501step1 line 467
  93. def OAI.MUB6.Certificate.PairSemantics.raw8501step2 line 469
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8501 line 471
  95. def OAI.MUB6.Certificate.PairSemantics.raw8502 line 489
  96. def OAI.MUB6.Certificate.PairSemantics.raw8502step0 line 491
  97. def OAI.MUB6.Certificate.PairSemantics.raw8502step1 line 493
  98. def OAI.MUB6.Certificate.PairSemantics.raw8502step2 line 495
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8502 line 497
  100. def OAI.MUB6.Certificate.PairSemantics.raw8503 line 515
  101. def OAI.MUB6.Certificate.PairSemantics.raw8503step0 line 517
  102. def OAI.MUB6.Certificate.PairSemantics.raw8503step1 line 519
  103. def OAI.MUB6.Certificate.PairSemantics.raw8503step2 line 521
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8503 line 523
  105. def OAI.MUB6.Certificate.PairSemantics.raw8504 line 541
  106. def OAI.MUB6.Certificate.PairSemantics.raw8504step0 line 543
  107. def OAI.MUB6.Certificate.PairSemantics.raw8504step1 line 545
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical8504 line 547
  109. def OAI.MUB6.Certificate.PairSemantics.raw8505 line 560
  110. def OAI.MUB6.Certificate.PairSemantics.raw8505step0 line 562
  111. def OAI.MUB6.Certificate.PairSemantics.raw8505step1 line 564
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical8505 line 566
  113. def OAI.MUB6.Certificate.PairSemantics.raw8506 line 579
  114. def OAI.MUB6.Certificate.PairSemantics.raw8506step0 line 581
  115. def OAI.MUB6.Certificate.PairSemantics.raw8506step1 line 583
  116. def OAI.MUB6.Certificate.PairSemantics.raw8506step2 line 585
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical8506 line 587
  118. def OAI.MUB6.Certificate.PairSemantics.raw8507 line 605
  119. def OAI.MUB6.Certificate.PairSemantics.raw8507step0 line 607
  120. def OAI.MUB6.Certificate.PairSemantics.raw8507step1 line 609
  121. def OAI.MUB6.Certificate.PairSemantics.raw8507step2 line 611
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical8507 line 613
  123. def OAI.MUB6.Certificate.PairSemantics.raw8508 line 631
  124. def OAI.MUB6.Certificate.PairSemantics.raw8508step0 line 633
  125. def OAI.MUB6.Certificate.PairSemantics.raw8508step1 line 635
  126. def OAI.MUB6.Certificate.PairSemantics.raw8508step2 line 637
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical8508 line 639
  128. def OAI.MUB6.Certificate.PairSemantics.raw8509 line 656
  129. def OAI.MUB6.Certificate.PairSemantics.raw8509step0 line 658
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical8509 line 660
  131. def OAI.MUB6.Certificate.PairSemantics.raw8510 line 669
  132. def OAI.MUB6.Certificate.PairSemantics.raw8510step0 line 671
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical8510 line 673
  134. def OAI.MUB6.Certificate.PairSemantics.raw8511 line 682
  135. def OAI.MUB6.Certificate.PairSemantics.raw8511step0 line 684
  136. theorem OAI.MUB6.Certificate.PairSemantics.canonical8511 line 686