OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical281.lean

GitHub source file

144 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8992 line 10
  2. def OAI.MUB6.Certificate.PairSemantics.raw8992step0 line 12
  3. def OAI.MUB6.Certificate.PairSemantics.raw8992step1 line 14
  4. def OAI.MUB6.Certificate.PairSemantics.raw8992step2 line 16
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical8992 line 18
  6. def OAI.MUB6.Certificate.PairSemantics.raw8993 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw8993step0 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw8993step1 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw8993step2 line 43
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8993 line 45
  11. def OAI.MUB6.Certificate.PairSemantics.raw8994 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw8994step0 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw8994step1 line 68
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8994 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw8995 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw8995step0 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw8995step1 line 88
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical8995 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw8996 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw8996step0 line 106
  21. def OAI.MUB6.Certificate.PairSemantics.raw8996step1 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw8996step2 line 110
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8996 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw8997 line 131
  25. def OAI.MUB6.Certificate.PairSemantics.raw8997step0 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw8997step1 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw8997step2 line 137
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8997 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw8998 line 158
  30. def OAI.MUB6.Certificate.PairSemantics.raw8998step0 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw8998step1 line 162
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical8998 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw8999 line 178
  34. def OAI.MUB6.Certificate.PairSemantics.raw8999step0 line 180
  35. def OAI.MUB6.Certificate.PairSemantics.raw8999step1 line 182
  36. def OAI.MUB6.Certificate.PairSemantics.raw8999step2 line 184
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical8999 line 186
  38. def OAI.MUB6.Certificate.PairSemantics.raw9000 line 205
  39. def OAI.MUB6.Certificate.PairSemantics.raw9000step0 line 207
  40. def OAI.MUB6.Certificate.PairSemantics.raw9000step1 line 209
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9000 line 211
  42. def OAI.MUB6.Certificate.PairSemantics.raw9001 line 225
  43. def OAI.MUB6.Certificate.PairSemantics.raw9001step0 line 227
  44. def OAI.MUB6.Certificate.PairSemantics.raw9001step1 line 229
  45. def OAI.MUB6.Certificate.PairSemantics.raw9001step2 line 231
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9001 line 233
  47. def OAI.MUB6.Certificate.PairSemantics.raw9002 line 252
  48. def OAI.MUB6.Certificate.PairSemantics.raw9002step0 line 254
  49. def OAI.MUB6.Certificate.PairSemantics.raw9002step1 line 256
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9002 line 258
  51. def OAI.MUB6.Certificate.PairSemantics.raw9003 line 272
  52. def OAI.MUB6.Certificate.PairSemantics.raw9003step0 line 274
  53. def OAI.MUB6.Certificate.PairSemantics.raw9003step1 line 276
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9003 line 278
  55. def OAI.MUB6.Certificate.PairSemantics.raw9004 line 292
  56. def OAI.MUB6.Certificate.PairSemantics.raw9004step0 line 294
  57. def OAI.MUB6.Certificate.PairSemantics.raw9004step1 line 296
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical9004 line 298
  59. def OAI.MUB6.Certificate.PairSemantics.raw9005 line 312
  60. def OAI.MUB6.Certificate.PairSemantics.raw9005step0 line 314
  61. def OAI.MUB6.Certificate.PairSemantics.raw9005step1 line 316
  62. def OAI.MUB6.Certificate.PairSemantics.raw9005step2 line 318
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9005 line 320
  64. def OAI.MUB6.Certificate.PairSemantics.raw9006 line 339
  65. def OAI.MUB6.Certificate.PairSemantics.raw9006step0 line 341
  66. def OAI.MUB6.Certificate.PairSemantics.raw9006step1 line 343
  67. def OAI.MUB6.Certificate.PairSemantics.raw9006step2 line 345
  68. def OAI.MUB6.Certificate.PairSemantics.raw9006step3 line 347
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9006 line 349
  70. def OAI.MUB6.Certificate.PairSemantics.raw9007 line 373
  71. def OAI.MUB6.Certificate.PairSemantics.raw9007step0 line 375
  72. def OAI.MUB6.Certificate.PairSemantics.raw9007step1 line 377
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical9007 line 379
  74. def OAI.MUB6.Certificate.PairSemantics.raw9008 line 394
  75. def OAI.MUB6.Certificate.PairSemantics.raw9008step0 line 396
  76. def OAI.MUB6.Certificate.PairSemantics.raw9008step1 line 398
  77. def OAI.MUB6.Certificate.PairSemantics.raw9008step2 line 400
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9008 line 402
  79. def OAI.MUB6.Certificate.PairSemantics.raw9009 line 421
  80. def OAI.MUB6.Certificate.PairSemantics.raw9009step0 line 423
  81. def OAI.MUB6.Certificate.PairSemantics.raw9009step1 line 425
  82. def OAI.MUB6.Certificate.PairSemantics.raw9009step2 line 427
  83. def OAI.MUB6.Certificate.PairSemantics.raw9009step3 line 429
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9009 line 431
  85. def OAI.MUB6.Certificate.PairSemantics.raw9010 line 455
  86. def OAI.MUB6.Certificate.PairSemantics.raw9010step0 line 457
  87. def OAI.MUB6.Certificate.PairSemantics.raw9010step1 line 459
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9010 line 461
  89. def OAI.MUB6.Certificate.PairSemantics.raw9011 line 476
  90. def OAI.MUB6.Certificate.PairSemantics.raw9011step0 line 478
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9011 line 480
  92. def OAI.MUB6.Certificate.PairSemantics.raw9012 line 490
  93. def OAI.MUB6.Certificate.PairSemantics.raw9012step0 line 492
  94. def OAI.MUB6.Certificate.PairSemantics.raw9012step1 line 494
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9012 line 496
  96. def OAI.MUB6.Certificate.PairSemantics.raw9013 line 511
  97. def OAI.MUB6.Certificate.PairSemantics.raw9013step0 line 513
  98. def OAI.MUB6.Certificate.PairSemantics.raw9013step1 line 515
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9013 line 517
  100. def OAI.MUB6.Certificate.PairSemantics.raw9014 line 531
  101. def OAI.MUB6.Certificate.PairSemantics.raw9014step0 line 533
  102. def OAI.MUB6.Certificate.PairSemantics.raw9014step1 line 535
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical9014 line 537
  104. def OAI.MUB6.Certificate.PairSemantics.raw9015 line 551
  105. def OAI.MUB6.Certificate.PairSemantics.raw9015step0 line 553
  106. def OAI.MUB6.Certificate.PairSemantics.raw9015step1 line 555
  107. def OAI.MUB6.Certificate.PairSemantics.raw9015step2 line 557
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical9015 line 559
  109. def OAI.MUB6.Certificate.PairSemantics.raw9016 line 578
  110. def OAI.MUB6.Certificate.PairSemantics.raw9016step0 line 580
  111. def OAI.MUB6.Certificate.PairSemantics.raw9016step1 line 582
  112. def OAI.MUB6.Certificate.PairSemantics.raw9016step2 line 584
  113. def OAI.MUB6.Certificate.PairSemantics.raw9016step3 line 586
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical9016 line 588
  115. def OAI.MUB6.Certificate.PairSemantics.raw9017 line 612
  116. def OAI.MUB6.Certificate.PairSemantics.raw9017step0 line 614
  117. def OAI.MUB6.Certificate.PairSemantics.raw9017step1 line 616
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical9017 line 618
  119. def OAI.MUB6.Certificate.PairSemantics.raw9018 line 632
  120. def OAI.MUB6.Certificate.PairSemantics.raw9018step0 line 634
  121. def OAI.MUB6.Certificate.PairSemantics.raw9018step1 line 636
  122. def OAI.MUB6.Certificate.PairSemantics.raw9018step2 line 638
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical9018 line 640
  124. def OAI.MUB6.Certificate.PairSemantics.raw9019 line 659
  125. def OAI.MUB6.Certificate.PairSemantics.raw9019step0 line 661
  126. def OAI.MUB6.Certificate.PairSemantics.raw9019step1 line 663
  127. def OAI.MUB6.Certificate.PairSemantics.raw9019step2 line 665
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical9019 line 667
  129. def OAI.MUB6.Certificate.PairSemantics.raw9020 line 687
  130. def OAI.MUB6.Certificate.PairSemantics.raw9020step0 line 689
  131. def OAI.MUB6.Certificate.PairSemantics.raw9020step1 line 691
  132. theorem OAI.MUB6.Certificate.PairSemantics.canonical9020 line 693
  133. def OAI.MUB6.Certificate.PairSemantics.raw9021 line 708
  134. def OAI.MUB6.Certificate.PairSemantics.raw9021step0 line 710
  135. theorem OAI.MUB6.Certificate.PairSemantics.canonical9021 line 712
  136. def OAI.MUB6.Certificate.PairSemantics.raw9022 line 722
  137. def OAI.MUB6.Certificate.PairSemantics.raw9022step0 line 724
  138. def OAI.MUB6.Certificate.PairSemantics.raw9022step1 line 726
  139. def OAI.MUB6.Certificate.PairSemantics.raw9022step2 line 728
  140. theorem OAI.MUB6.Certificate.PairSemantics.canonical9022 line 730
  141. def OAI.MUB6.Certificate.PairSemantics.raw9023 line 749
  142. def OAI.MUB6.Certificate.PairSemantics.raw9023step0 line 751
  143. def OAI.MUB6.Certificate.PairSemantics.raw9023step1 line 753
  144. theorem OAI.MUB6.Certificate.PairSemantics.canonical9023 line 755