OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical305.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9760 line 25
  2. def OAI.MUB6.Certificate.PairSemantics.raw9760step0 line 27
  3. def OAI.MUB6.Certificate.PairSemantics.raw9760step1 line 29
  4. def OAI.MUB6.Certificate.PairSemantics.raw9760step2 line 31
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical9760 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw9761 line 50
  7. def OAI.MUB6.Certificate.PairSemantics.raw9761step0 line 52
  8. def OAI.MUB6.Certificate.PairSemantics.raw9761step1 line 54
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9761 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw9762 line 69
  11. def OAI.MUB6.Certificate.PairSemantics.raw9762step0 line 71
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9762 line 73
  13. def OAI.MUB6.Certificate.PairSemantics.raw9763 line 82
  14. def OAI.MUB6.Certificate.PairSemantics.raw9763step0 line 84
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9763 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw9764 line 95
  17. def OAI.MUB6.Certificate.PairSemantics.raw9764step0 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw9764step1 line 99
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9764 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw9765 line 115
  21. def OAI.MUB6.Certificate.PairSemantics.raw9765step0 line 117
  22. def OAI.MUB6.Certificate.PairSemantics.raw9765step1 line 119
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9765 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw9766 line 135
  25. def OAI.MUB6.Certificate.PairSemantics.raw9766step0 line 137
  26. def OAI.MUB6.Certificate.PairSemantics.raw9766step1 line 139
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical9766 line 141
  28. def OAI.MUB6.Certificate.PairSemantics.raw9767 line 155
  29. def OAI.MUB6.Certificate.PairSemantics.raw9767step0 line 157
  30. def OAI.MUB6.Certificate.PairSemantics.raw9767step1 line 159
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9767 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw9768 line 175
  33. def OAI.MUB6.Certificate.PairSemantics.raw9768step0 line 177
  34. def OAI.MUB6.Certificate.PairSemantics.raw9768step1 line 179
  35. def OAI.MUB6.Certificate.PairSemantics.raw9768step2 line 181
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical9768 line 183
  37. def OAI.MUB6.Certificate.PairSemantics.raw9769 line 201
  38. def OAI.MUB6.Certificate.PairSemantics.raw9769step0 line 203
  39. def OAI.MUB6.Certificate.PairSemantics.raw9769step1 line 205
  40. def OAI.MUB6.Certificate.PairSemantics.raw9769step2 line 207
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9769 line 209
  42. def OAI.MUB6.Certificate.PairSemantics.raw9770 line 227
  43. def OAI.MUB6.Certificate.PairSemantics.raw9770step0 line 229
  44. def OAI.MUB6.Certificate.PairSemantics.raw9770step1 line 231
  45. def OAI.MUB6.Certificate.PairSemantics.raw9770step2 line 233
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9770 line 235
  47. def OAI.MUB6.Certificate.PairSemantics.raw9771 line 253
  48. def OAI.MUB6.Certificate.PairSemantics.raw9771step0 line 255
  49. def OAI.MUB6.Certificate.PairSemantics.raw9771step1 line 257
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9771 line 259
  51. def OAI.MUB6.Certificate.PairSemantics.raw9772 line 273
  52. def OAI.MUB6.Certificate.PairSemantics.raw9772step0 line 275
  53. def OAI.MUB6.Certificate.PairSemantics.raw9772step1 line 277
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9772 line 279
  55. def OAI.MUB6.Certificate.PairSemantics.raw9773 line 293
  56. def OAI.MUB6.Certificate.PairSemantics.raw9773step0 line 295
  57. def OAI.MUB6.Certificate.PairSemantics.raw9773step1 line 297
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical9773 line 299
  59. def OAI.MUB6.Certificate.PairSemantics.raw9774 line 313
  60. def OAI.MUB6.Certificate.PairSemantics.raw9774step0 line 315
  61. def OAI.MUB6.Certificate.PairSemantics.raw9774step1 line 317
  62. def OAI.MUB6.Certificate.PairSemantics.raw9774step2 line 319
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9774 line 321
  64. def OAI.MUB6.Certificate.PairSemantics.raw9775 line 339
  65. def OAI.MUB6.Certificate.PairSemantics.raw9775step0 line 341
  66. def OAI.MUB6.Certificate.PairSemantics.raw9775step1 line 343
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9775 line 345
  68. def OAI.MUB6.Certificate.PairSemantics.raw9776 line 359
  69. def OAI.MUB6.Certificate.PairSemantics.raw9776step0 line 361
  70. def OAI.MUB6.Certificate.PairSemantics.raw9776step1 line 363
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9776 line 365
  72. def OAI.MUB6.Certificate.PairSemantics.raw9777 line 379
  73. def OAI.MUB6.Certificate.PairSemantics.raw9777step0 line 381
  74. def OAI.MUB6.Certificate.PairSemantics.raw9777step1 line 383
  75. def OAI.MUB6.Certificate.PairSemantics.raw9777step2 line 385
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical9777 line 387
  77. def OAI.MUB6.Certificate.PairSemantics.raw9778 line 405
  78. def OAI.MUB6.Certificate.PairSemantics.raw9778step0 line 407
  79. def OAI.MUB6.Certificate.PairSemantics.raw9778step1 line 409
  80. def OAI.MUB6.Certificate.PairSemantics.raw9778step2 line 411
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9778 line 413
  82. def OAI.MUB6.Certificate.PairSemantics.raw9779 line 431
  83. def OAI.MUB6.Certificate.PairSemantics.raw9779step0 line 433
  84. def OAI.MUB6.Certificate.PairSemantics.raw9779step1 line 435
  85. def OAI.MUB6.Certificate.PairSemantics.raw9779step2 line 437
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9779 line 439
  87. def OAI.MUB6.Certificate.PairSemantics.raw9780 line 457
  88. def OAI.MUB6.Certificate.PairSemantics.raw9780step0 line 459
  89. def OAI.MUB6.Certificate.PairSemantics.raw9780step1 line 461
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical9780 line 463
  91. def OAI.MUB6.Certificate.PairSemantics.raw9781 line 477
  92. def OAI.MUB6.Certificate.PairSemantics.raw9781step0 line 479
  93. def OAI.MUB6.Certificate.PairSemantics.raw9781step1 line 481
  94. def OAI.MUB6.Certificate.PairSemantics.raw9781step2 line 483
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9781 line 485
  96. def OAI.MUB6.Certificate.PairSemantics.raw9782 line 503
  97. def OAI.MUB6.Certificate.PairSemantics.raw9782step0 line 505
  98. def OAI.MUB6.Certificate.PairSemantics.raw9782step1 line 507
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9782 line 509
  100. def OAI.MUB6.Certificate.PairSemantics.raw9783 line 523
  101. def OAI.MUB6.Certificate.PairSemantics.raw9783step0 line 525
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9783 line 527
  103. def OAI.MUB6.Certificate.PairSemantics.raw9784 line 536
  104. def OAI.MUB6.Certificate.PairSemantics.raw9784step0 line 538
  105. def OAI.MUB6.Certificate.PairSemantics.raw9784step1 line 540
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical9784 line 542
  107. def OAI.MUB6.Certificate.PairSemantics.raw9785 line 555
  108. def OAI.MUB6.Certificate.PairSemantics.raw9785step0 line 557
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical9785 line 559
  110. def OAI.MUB6.Certificate.PairSemantics.raw9786 line 568
  111. def OAI.MUB6.Certificate.PairSemantics.raw9786step0 line 570
  112. def OAI.MUB6.Certificate.PairSemantics.raw9786step1 line 572
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical9786 line 574
  114. def OAI.MUB6.Certificate.PairSemantics.raw9787 line 587
  115. def OAI.MUB6.Certificate.PairSemantics.raw9787step0 line 589
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical9787 line 591
  117. def OAI.MUB6.Certificate.PairSemantics.raw9788 line 600
  118. def OAI.MUB6.Certificate.PairSemantics.raw9788step0 line 602
  119. def OAI.MUB6.Certificate.PairSemantics.raw9788step1 line 604
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical9788 line 606
  121. def OAI.MUB6.Certificate.PairSemantics.raw9789 line 620
  122. def OAI.MUB6.Certificate.PairSemantics.raw9789step0 line 622
  123. def OAI.MUB6.Certificate.PairSemantics.raw9789step1 line 624
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical9789 line 626
  125. def OAI.MUB6.Certificate.PairSemantics.raw9790 line 640
  126. def OAI.MUB6.Certificate.PairSemantics.raw9790step0 line 642
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical9790 line 644
  128. def OAI.MUB6.Certificate.PairSemantics.raw9791 line 653
  129. def OAI.MUB6.Certificate.PairSemantics.raw9791step0 line 655
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical9791 line 657