OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical280.lean

GitHub source file

141 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8960 line 9
  2. def OAI.MUB6.Certificate.PairSemantics.raw8960step0 line 11
  3. def OAI.MUB6.Certificate.PairSemantics.raw8960step1 line 13
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8960 line 15
  5. def OAI.MUB6.Certificate.PairSemantics.raw8961 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw8961step0 line 32
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical8961 line 34
  8. def OAI.MUB6.Certificate.PairSemantics.raw8962 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw8962step0 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8962 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw8963 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw8963step0 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw8963step1 line 62
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8963 line 64
  15. def OAI.MUB6.Certificate.PairSemantics.raw8964 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw8964step0 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw8964step1 line 83
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical8964 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw8965 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw8965step0 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw8965step1 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw8965step2 line 105
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8965 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw8966 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw8966step0 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw8966step1 line 130
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical8966 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw8967 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw8967step0 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw8967step1 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw8967step2 line 152
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical8967 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw8968 line 173
  34. def OAI.MUB6.Certificate.PairSemantics.raw8968step0 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw8968step1 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw8968step2 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw8968step3 line 181
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8968 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw8969 line 208
  40. def OAI.MUB6.Certificate.PairSemantics.raw8969step0 line 210
  41. def OAI.MUB6.Certificate.PairSemantics.raw8969step1 line 212
  42. def OAI.MUB6.Certificate.PairSemantics.raw8969step2 line 214
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical8969 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw8970 line 236
  45. def OAI.MUB6.Certificate.PairSemantics.raw8970step0 line 238
  46. def OAI.MUB6.Certificate.PairSemantics.raw8970step1 line 240
  47. def OAI.MUB6.Certificate.PairSemantics.raw8970step2 line 242
  48. def OAI.MUB6.Certificate.PairSemantics.raw8970step3 line 244
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8970 line 246
  50. def OAI.MUB6.Certificate.PairSemantics.raw8971 line 271
  51. def OAI.MUB6.Certificate.PairSemantics.raw8971step0 line 273
  52. def OAI.MUB6.Certificate.PairSemantics.raw8971step1 line 275
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8971 line 277
  54. def OAI.MUB6.Certificate.PairSemantics.raw8972 line 292
  55. def OAI.MUB6.Certificate.PairSemantics.raw8972step0 line 294
  56. def OAI.MUB6.Certificate.PairSemantics.raw8972step1 line 296
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8972 line 298
  58. def OAI.MUB6.Certificate.PairSemantics.raw8973 line 313
  59. def OAI.MUB6.Certificate.PairSemantics.raw8973step0 line 315
  60. def OAI.MUB6.Certificate.PairSemantics.raw8973step1 line 317
  61. def OAI.MUB6.Certificate.PairSemantics.raw8973step2 line 319
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8973 line 321
  63. def OAI.MUB6.Certificate.PairSemantics.raw8974 line 341
  64. def OAI.MUB6.Certificate.PairSemantics.raw8974step0 line 343
  65. def OAI.MUB6.Certificate.PairSemantics.raw8974step1 line 345
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8974 line 347
  67. def OAI.MUB6.Certificate.PairSemantics.raw8975 line 361
  68. def OAI.MUB6.Certificate.PairSemantics.raw8975step0 line 363
  69. def OAI.MUB6.Certificate.PairSemantics.raw8975step1 line 365
  70. def OAI.MUB6.Certificate.PairSemantics.raw8975step2 line 367
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8975 line 369
  72. def OAI.MUB6.Certificate.PairSemantics.raw8976 line 388
  73. def OAI.MUB6.Certificate.PairSemantics.raw8976step0 line 390
  74. def OAI.MUB6.Certificate.PairSemantics.raw8976step1 line 392
  75. def OAI.MUB6.Certificate.PairSemantics.raw8976step2 line 394
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8976 line 396
  77. def OAI.MUB6.Certificate.PairSemantics.raw8977 line 415
  78. def OAI.MUB6.Certificate.PairSemantics.raw8977step0 line 417
  79. def OAI.MUB6.Certificate.PairSemantics.raw8977step1 line 419
  80. def OAI.MUB6.Certificate.PairSemantics.raw8977step2 line 421
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8977 line 423
  82. def OAI.MUB6.Certificate.PairSemantics.raw8978 line 443
  83. def OAI.MUB6.Certificate.PairSemantics.raw8978step0 line 445
  84. def OAI.MUB6.Certificate.PairSemantics.raw8978step1 line 447
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8978 line 449
  86. def OAI.MUB6.Certificate.PairSemantics.raw8979 line 464
  87. def OAI.MUB6.Certificate.PairSemantics.raw8979step0 line 466
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical8979 line 468
  89. def OAI.MUB6.Certificate.PairSemantics.raw8980 line 478
  90. def OAI.MUB6.Certificate.PairSemantics.raw8980step0 line 480
  91. def OAI.MUB6.Certificate.PairSemantics.raw8980step1 line 482
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical8980 line 484
  93. def OAI.MUB6.Certificate.PairSemantics.raw8981 line 498
  94. def OAI.MUB6.Certificate.PairSemantics.raw8981step0 line 500
  95. def OAI.MUB6.Certificate.PairSemantics.raw8981step1 line 502
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8981 line 504
  97. def OAI.MUB6.Certificate.PairSemantics.raw8982 line 519
  98. def OAI.MUB6.Certificate.PairSemantics.raw8982step0 line 521
  99. def OAI.MUB6.Certificate.PairSemantics.raw8982step1 line 523
  100. def OAI.MUB6.Certificate.PairSemantics.raw8982step2 line 525
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8982 line 527
  102. def OAI.MUB6.Certificate.PairSemantics.raw8983 line 547
  103. def OAI.MUB6.Certificate.PairSemantics.raw8983step0 line 549
  104. def OAI.MUB6.Certificate.PairSemantics.raw8983step1 line 551
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical8983 line 553
  106. def OAI.MUB6.Certificate.PairSemantics.raw8984 line 567
  107. def OAI.MUB6.Certificate.PairSemantics.raw8984step0 line 569
  108. def OAI.MUB6.Certificate.PairSemantics.raw8984step1 line 571
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical8984 line 573
  110. def OAI.MUB6.Certificate.PairSemantics.raw8985 line 587
  111. def OAI.MUB6.Certificate.PairSemantics.raw8985step0 line 589
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical8985 line 591
  113. def OAI.MUB6.Certificate.PairSemantics.raw8986 line 601
  114. def OAI.MUB6.Certificate.PairSemantics.raw8986step0 line 603
  115. def OAI.MUB6.Certificate.PairSemantics.raw8986step1 line 605
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical8986 line 607
  117. def OAI.MUB6.Certificate.PairSemantics.raw8987 line 621
  118. def OAI.MUB6.Certificate.PairSemantics.raw8987step0 line 623
  119. def OAI.MUB6.Certificate.PairSemantics.raw8987step1 line 625
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8987 line 627
  121. def OAI.MUB6.Certificate.PairSemantics.raw8988 line 642
  122. def OAI.MUB6.Certificate.PairSemantics.raw8988step0 line 644
  123. def OAI.MUB6.Certificate.PairSemantics.raw8988step1 line 646
  124. def OAI.MUB6.Certificate.PairSemantics.raw8988step2 line 648
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical8988 line 650
  126. def OAI.MUB6.Certificate.PairSemantics.raw8989 line 670
  127. def OAI.MUB6.Certificate.PairSemantics.raw8989step0 line 672
  128. def OAI.MUB6.Certificate.PairSemantics.raw8989step1 line 674
  129. def OAI.MUB6.Certificate.PairSemantics.raw8989step2 line 676
  130. def OAI.MUB6.Certificate.PairSemantics.raw8989step3 line 678
  131. theorem OAI.MUB6.Certificate.PairSemantics.canonical8989 line 680
  132. def OAI.MUB6.Certificate.PairSemantics.raw8990 line 705
  133. def OAI.MUB6.Certificate.PairSemantics.raw8990step0 line 707
  134. def OAI.MUB6.Certificate.PairSemantics.raw8990step1 line 709
  135. def OAI.MUB6.Certificate.PairSemantics.raw8990step2 line 711
  136. theorem OAI.MUB6.Certificate.PairSemantics.canonical8990 line 713
  137. def OAI.MUB6.Certificate.PairSemantics.raw8991 line 732
  138. def OAI.MUB6.Certificate.PairSemantics.raw8991step0 line 734
  139. def OAI.MUB6.Certificate.PairSemantics.raw8991step1 line 736
  140. def OAI.MUB6.Certificate.PairSemantics.raw8991step2 line 738
  141. theorem OAI.MUB6.Certificate.PairSemantics.canonical8991 line 740