OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical277.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8864 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8864step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw8864step1 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw8864step2 line 25
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical8864 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw8865 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw8865step0 line 46
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8865 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw8866 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw8866step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw8866step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8866 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw8867 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw8867step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw8867step1 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8867 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw8868 line 96
  18. def OAI.MUB6.Certificate.PairSemantics.raw8868step0 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw8868step1 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8868 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw8869 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw8869step0 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw8869step1 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw8869step2 line 122
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8869 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw8870 line 142
  27. def OAI.MUB6.Certificate.PairSemantics.raw8870step0 line 144
  28. def OAI.MUB6.Certificate.PairSemantics.raw8870step1 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw8870step2 line 148
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8870 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw8871 line 167
  32. def OAI.MUB6.Certificate.PairSemantics.raw8871step0 line 169
  33. def OAI.MUB6.Certificate.PairSemantics.raw8871step1 line 171
  34. def OAI.MUB6.Certificate.PairSemantics.raw8871step2 line 173
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8871 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw8872 line 193
  37. def OAI.MUB6.Certificate.PairSemantics.raw8872step0 line 195
  38. def OAI.MUB6.Certificate.PairSemantics.raw8872step1 line 197
  39. def OAI.MUB6.Certificate.PairSemantics.raw8872step2 line 199
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8872 line 201
  41. def OAI.MUB6.Certificate.PairSemantics.raw8873 line 218
  42. def OAI.MUB6.Certificate.PairSemantics.raw8873step0 line 220
  43. def OAI.MUB6.Certificate.PairSemantics.raw8873step1 line 222
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8873 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw8874 line 237
  46. def OAI.MUB6.Certificate.PairSemantics.raw8874step0 line 239
  47. def OAI.MUB6.Certificate.PairSemantics.raw8874step1 line 241
  48. def OAI.MUB6.Certificate.PairSemantics.raw8874step2 line 243
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8874 line 245
  50. def OAI.MUB6.Certificate.PairSemantics.raw8875 line 263
  51. def OAI.MUB6.Certificate.PairSemantics.raw8875step0 line 265
  52. def OAI.MUB6.Certificate.PairSemantics.raw8875step1 line 267
  53. def OAI.MUB6.Certificate.PairSemantics.raw8875step2 line 269
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical8875 line 271
  55. def OAI.MUB6.Certificate.PairSemantics.raw8876 line 289
  56. def OAI.MUB6.Certificate.PairSemantics.raw8876step0 line 291
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8876 line 293
  58. def OAI.MUB6.Certificate.PairSemantics.raw8877 line 302
  59. def OAI.MUB6.Certificate.PairSemantics.raw8877step0 line 304
  60. def OAI.MUB6.Certificate.PairSemantics.raw8877step1 line 306
  61. def OAI.MUB6.Certificate.PairSemantics.raw8877step2 line 308
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8877 line 310
  63. def OAI.MUB6.Certificate.PairSemantics.raw8878 line 328
  64. def OAI.MUB6.Certificate.PairSemantics.raw8878step0 line 330
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8878 line 332
  66. def OAI.MUB6.Certificate.PairSemantics.raw8879 line 341
  67. def OAI.MUB6.Certificate.PairSemantics.raw8879step0 line 343
  68. def OAI.MUB6.Certificate.PairSemantics.raw8879step1 line 345
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8879 line 347
  70. def OAI.MUB6.Certificate.PairSemantics.raw8880 line 361
  71. def OAI.MUB6.Certificate.PairSemantics.raw8880step0 line 363
  72. def OAI.MUB6.Certificate.PairSemantics.raw8880step1 line 365
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8880 line 367
  74. def OAI.MUB6.Certificate.PairSemantics.raw8881 line 380
  75. def OAI.MUB6.Certificate.PairSemantics.raw8881step0 line 382
  76. def OAI.MUB6.Certificate.PairSemantics.raw8881step1 line 384
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8881 line 386
  78. def OAI.MUB6.Certificate.PairSemantics.raw8882 line 399
  79. def OAI.MUB6.Certificate.PairSemantics.raw8882step0 line 401
  80. def OAI.MUB6.Certificate.PairSemantics.raw8882step1 line 403
  81. def OAI.MUB6.Certificate.PairSemantics.raw8882step2 line 405
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8882 line 407
  83. def OAI.MUB6.Certificate.PairSemantics.raw8883 line 424
  84. def OAI.MUB6.Certificate.PairSemantics.raw8883step0 line 426
  85. def OAI.MUB6.Certificate.PairSemantics.raw8883step1 line 428
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8883 line 430
  87. def OAI.MUB6.Certificate.PairSemantics.raw8884 line 443
  88. def OAI.MUB6.Certificate.PairSemantics.raw8884step0 line 445
  89. def OAI.MUB6.Certificate.PairSemantics.raw8884step1 line 447
  90. def OAI.MUB6.Certificate.PairSemantics.raw8884step2 line 449
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8884 line 451
  92. def OAI.MUB6.Certificate.PairSemantics.raw8885 line 468
  93. def OAI.MUB6.Certificate.PairSemantics.raw8885step0 line 470
  94. def OAI.MUB6.Certificate.PairSemantics.raw8885step1 line 472
  95. def OAI.MUB6.Certificate.PairSemantics.raw8885step2 line 474
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8885 line 476
  97. def OAI.MUB6.Certificate.PairSemantics.raw8886 line 493
  98. def OAI.MUB6.Certificate.PairSemantics.raw8886step0 line 495
  99. def OAI.MUB6.Certificate.PairSemantics.raw8886step1 line 497
  100. def OAI.MUB6.Certificate.PairSemantics.raw8886step2 line 499
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8886 line 501
  102. def OAI.MUB6.Certificate.PairSemantics.raw8887 line 518
  103. def OAI.MUB6.Certificate.PairSemantics.raw8887step0 line 520
  104. def OAI.MUB6.Certificate.PairSemantics.raw8887step1 line 522
  105. def OAI.MUB6.Certificate.PairSemantics.raw8887step2 line 524
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8887 line 526
  107. def OAI.MUB6.Certificate.PairSemantics.raw8888 line 543
  108. def OAI.MUB6.Certificate.PairSemantics.raw8888step0 line 545
  109. def OAI.MUB6.Certificate.PairSemantics.raw8888step1 line 547
  110. def OAI.MUB6.Certificate.PairSemantics.raw8888step2 line 549
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical8888 line 551
  112. def OAI.MUB6.Certificate.PairSemantics.raw8889 line 568
  113. def OAI.MUB6.Certificate.PairSemantics.raw8889step0 line 570
  114. def OAI.MUB6.Certificate.PairSemantics.raw8889step1 line 572
  115. def OAI.MUB6.Certificate.PairSemantics.raw8889step2 line 574
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical8889 line 576
  117. def OAI.MUB6.Certificate.PairSemantics.raw8890 line 593
  118. def OAI.MUB6.Certificate.PairSemantics.raw8890step0 line 595
  119. def OAI.MUB6.Certificate.PairSemantics.raw8890step1 line 597
  120. def OAI.MUB6.Certificate.PairSemantics.raw8890step2 line 599
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical8890 line 601
  122. def OAI.MUB6.Certificate.PairSemantics.raw8891 line 618
  123. def OAI.MUB6.Certificate.PairSemantics.raw8891step0 line 620
  124. def OAI.MUB6.Certificate.PairSemantics.raw8891step1 line 622
  125. def OAI.MUB6.Certificate.PairSemantics.raw8891step2 line 624
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical8891 line 626
  127. def OAI.MUB6.Certificate.PairSemantics.raw8892 line 643
  128. def OAI.MUB6.Certificate.PairSemantics.raw8892step0 line 645
  129. def OAI.MUB6.Certificate.PairSemantics.raw8892step1 line 647
  130. def OAI.MUB6.Certificate.PairSemantics.raw8892step2 line 649
  131. theorem OAI.MUB6.Certificate.PairSemantics.canonical8892 line 651
  132. def OAI.MUB6.Certificate.PairSemantics.raw8893 line 668
  133. def OAI.MUB6.Certificate.PairSemantics.raw8893step0 line 670
  134. def OAI.MUB6.Certificate.PairSemantics.raw8893step1 line 672
  135. def OAI.MUB6.Certificate.PairSemantics.raw8893step2 line 674
  136. theorem OAI.MUB6.Certificate.PairSemantics.canonical8893 line 676
  137. def OAI.MUB6.Certificate.PairSemantics.raw8894 line 693
  138. def OAI.MUB6.Certificate.PairSemantics.raw8894step0 line 695
  139. def OAI.MUB6.Certificate.PairSemantics.raw8894step1 line 697
  140. def OAI.MUB6.Certificate.PairSemantics.raw8894step2 line 699
  141. theorem OAI.MUB6.Certificate.PairSemantics.canonical8894 line 701
  142. def OAI.MUB6.Certificate.PairSemantics.raw8895 line 718
  143. def OAI.MUB6.Certificate.PairSemantics.raw8895step0 line 720
  144. def OAI.MUB6.Certificate.PairSemantics.raw8895step1 line 722
  145. def OAI.MUB6.Certificate.PairSemantics.raw8895step2 line 724
  146. theorem OAI.MUB6.Certificate.PairSemantics.canonical8895 line 726