OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound10.lean

GitHub source file

150 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation640 line 41
  2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix640 line 47
  3. theorem OAI.MUB6.Certificate.PairSemantics.sound640 line 49
  4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation641 line 84
  5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix641 line 90
  6. theorem OAI.MUB6.Certificate.PairSemantics.sound641 line 92
  7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation642 line 127
  8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix642 line 133
  9. theorem OAI.MUB6.Certificate.PairSemantics.sound642 line 135
  10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation643 line 170
  11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix643 line 176
  12. theorem OAI.MUB6.Certificate.PairSemantics.sound643 line 178
  13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation644 line 213
  14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix644 line 219
  15. theorem OAI.MUB6.Certificate.PairSemantics.sound644 line 221
  16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation645 line 256
  17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix645 line 262
  18. theorem OAI.MUB6.Certificate.PairSemantics.sound645 line 264
  19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation646 line 299
  20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix646 line 305
  21. theorem OAI.MUB6.Certificate.PairSemantics.sound646 line 307
  22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation647 line 342
  23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix647 line 348
  24. theorem OAI.MUB6.Certificate.PairSemantics.sound647 line 350
  25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation648 line 385
  26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix648 line 391
  27. theorem OAI.MUB6.Certificate.PairSemantics.sound648 line 393
  28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation649 line 428
  29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix649 line 434
  30. theorem OAI.MUB6.Certificate.PairSemantics.sound649 line 436
  31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation650 line 471
  32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix650 line 477
  33. theorem OAI.MUB6.Certificate.PairSemantics.sound650 line 479
  34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation651 line 514
  35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix651 line 520
  36. theorem OAI.MUB6.Certificate.PairSemantics.sound651 line 522
  37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation652 line 557
  38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix652 line 563
  39. theorem OAI.MUB6.Certificate.PairSemantics.sound652 line 565
  40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation653 line 600
  41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix653 line 606
  42. theorem OAI.MUB6.Certificate.PairSemantics.sound653 line 608
  43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation654 line 643
  44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix654 line 649
  45. theorem OAI.MUB6.Certificate.PairSemantics.sound654 line 651
  46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation655 line 686
  47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix655 line 692
  48. theorem OAI.MUB6.Certificate.PairSemantics.sound655 line 694
  49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation656 line 729
  50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix656 line 735
  51. theorem OAI.MUB6.Certificate.PairSemantics.sound656 line 737
  52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation657 line 772
  53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix657 line 778
  54. theorem OAI.MUB6.Certificate.PairSemantics.sound657 line 780
  55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation658 line 815
  56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix658 line 821
  57. theorem OAI.MUB6.Certificate.PairSemantics.sound658 line 823
  58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation659 line 858
  59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix659 line 864
  60. theorem OAI.MUB6.Certificate.PairSemantics.sound659 line 866
  61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation660 line 901
  62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix660 line 907
  63. theorem OAI.MUB6.Certificate.PairSemantics.sound660 line 909
  64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation661 line 944
  65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix661 line 950
  66. theorem OAI.MUB6.Certificate.PairSemantics.sound661 line 952
  67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation662 line 987
  68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix662 line 993
  69. theorem OAI.MUB6.Certificate.PairSemantics.sound662 line 995
  70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation663 line 1030
  71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix663 line 1036
  72. theorem OAI.MUB6.Certificate.PairSemantics.sound663 line 1038
  73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation664 line 1073
  74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix664 line 1079
  75. theorem OAI.MUB6.Certificate.PairSemantics.sound664 line 1081
  76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation665 line 1116
  77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix665 line 1122
  78. theorem OAI.MUB6.Certificate.PairSemantics.sound665 line 1124
  79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation666 line 1159
  80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix666 line 1165
  81. theorem OAI.MUB6.Certificate.PairSemantics.sound666 line 1167
  82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation667 line 1202
  83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix667 line 1208
  84. theorem OAI.MUB6.Certificate.PairSemantics.sound667 line 1210
  85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation668 line 1245
  86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix668 line 1251
  87. theorem OAI.MUB6.Certificate.PairSemantics.sound668 line 1253
  88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation669 line 1288
  89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix669 line 1294
  90. theorem OAI.MUB6.Certificate.PairSemantics.sound669 line 1296
  91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation670 line 1331
  92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix670 line 1337
  93. theorem OAI.MUB6.Certificate.PairSemantics.sound670 line 1339
  94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation671 line 1374
  95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix671 line 1380
  96. theorem OAI.MUB6.Certificate.PairSemantics.sound671 line 1382
  97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation672 line 1417
  98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix672 line 1423
  99. theorem OAI.MUB6.Certificate.PairSemantics.sound672 line 1425
  100. theorem OAI.MUB6.Certificate.PairSemantics.sound673 line 1460
  101. theorem OAI.MUB6.Certificate.PairSemantics.sound674 line 1465
  102. theorem OAI.MUB6.Certificate.PairSemantics.sound675 line 1470
  103. theorem OAI.MUB6.Certificate.PairSemantics.sound676 line 1475
  104. theorem OAI.MUB6.Certificate.PairSemantics.sound677 line 1480
  105. theorem OAI.MUB6.Certificate.PairSemantics.sound678 line 1485
  106. theorem OAI.MUB6.Certificate.PairSemantics.sound679 line 1490
  107. theorem OAI.MUB6.Certificate.PairSemantics.sound680 line 1495
  108. theorem OAI.MUB6.Certificate.PairSemantics.sound681 line 1500
  109. theorem OAI.MUB6.Certificate.PairSemantics.sound682 line 1505
  110. theorem OAI.MUB6.Certificate.PairSemantics.sound683 line 1510
  111. theorem OAI.MUB6.Certificate.PairSemantics.sound684 line 1515
  112. theorem OAI.MUB6.Certificate.PairSemantics.sound685 line 1520
  113. theorem OAI.MUB6.Certificate.PairSemantics.sound686 line 1525
  114. theorem OAI.MUB6.Certificate.PairSemantics.sound687 line 1530
  115. theorem OAI.MUB6.Certificate.PairSemantics.sound688 line 1535
  116. theorem OAI.MUB6.Certificate.PairSemantics.sound689 line 1540
  117. theorem OAI.MUB6.Certificate.PairSemantics.sound690 line 1545
  118. theorem OAI.MUB6.Certificate.PairSemantics.sound691 line 1550
  119. theorem OAI.MUB6.Certificate.PairSemantics.sound692 line 1555
  120. theorem OAI.MUB6.Certificate.PairSemantics.sound693 line 1560
  121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation694 line 1565
  122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix694 line 1571
  123. theorem OAI.MUB6.Certificate.PairSemantics.sound694 line 1573
  124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation695 line 1608
  125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix695 line 1614
  126. theorem OAI.MUB6.Certificate.PairSemantics.sound695 line 1616
  127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation696 line 1651
  128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix696 line 1657
  129. theorem OAI.MUB6.Certificate.PairSemantics.sound696 line 1659
  130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation697 line 1694
  131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix697 line 1700
  132. theorem OAI.MUB6.Certificate.PairSemantics.sound697 line 1702
  133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation698 line 1737
  134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix698 line 1743
  135. theorem OAI.MUB6.Certificate.PairSemantics.sound698 line 1745
  136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation699 line 1780
  137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix699 line 1786
  138. theorem OAI.MUB6.Certificate.PairSemantics.sound699 line 1788
  139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation700 line 1823
  140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix700 line 1829
  141. theorem OAI.MUB6.Certificate.PairSemantics.sound700 line 1831
  142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation701 line 1866
  143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix701 line 1872
  144. theorem OAI.MUB6.Certificate.PairSemantics.sound701 line 1874
  145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation702 line 1909
  146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix702 line 1915
  147. theorem OAI.MUB6.Certificate.PairSemantics.sound702 line 1917
  148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation703 line 1952
  149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix703 line 1958
  150. theorem OAI.MUB6.Certificate.PairSemantics.sound703 line 1960