OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound2.lean

GitHub source file

156 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation128 line 36
  2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix128 line 42
  3. theorem OAI.MUB6.Certificate.PairSemantics.sound128 line 44
  4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation129 line 74
  5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix129 line 80
  6. theorem OAI.MUB6.Certificate.PairSemantics.sound129 line 82
  7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation130 line 112
  8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix130 line 118
  9. theorem OAI.MUB6.Certificate.PairSemantics.sound130 line 120
  10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation131 line 150
  11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix131 line 156
  12. theorem OAI.MUB6.Certificate.PairSemantics.sound131 line 158
  13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation132 line 188
  14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix132 line 194
  15. theorem OAI.MUB6.Certificate.PairSemantics.sound132 line 196
  16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation133 line 226
  17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix133 line 232
  18. theorem OAI.MUB6.Certificate.PairSemantics.sound133 line 234
  19. theorem OAI.MUB6.Certificate.PairSemantics.sound134 line 264
  20. theorem OAI.MUB6.Certificate.PairSemantics.sound135 line 269
  21. theorem OAI.MUB6.Certificate.PairSemantics.sound136 line 274
  22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation137 line 279
  23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix137 line 285
  24. theorem OAI.MUB6.Certificate.PairSemantics.sound137 line 287
  25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation138 line 317
  26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix138 line 323
  27. theorem OAI.MUB6.Certificate.PairSemantics.sound138 line 325
  28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation139 line 355
  29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix139 line 361
  30. theorem OAI.MUB6.Certificate.PairSemantics.sound139 line 363
  31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation140 line 393
  32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix140 line 399
  33. theorem OAI.MUB6.Certificate.PairSemantics.sound140 line 401
  34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation141 line 431
  35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix141 line 437
  36. theorem OAI.MUB6.Certificate.PairSemantics.sound141 line 439
  37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation142 line 469
  38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix142 line 475
  39. theorem OAI.MUB6.Certificate.PairSemantics.sound142 line 477
  40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation143 line 507
  41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix143 line 513
  42. theorem OAI.MUB6.Certificate.PairSemantics.sound143 line 515
  43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation144 line 545
  44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix144 line 551
  45. theorem OAI.MUB6.Certificate.PairSemantics.sound144 line 553
  46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation145 line 583
  47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix145 line 589
  48. theorem OAI.MUB6.Certificate.PairSemantics.sound145 line 591
  49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation146 line 621
  50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix146 line 627
  51. theorem OAI.MUB6.Certificate.PairSemantics.sound146 line 629
  52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation147 line 659
  53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix147 line 665
  54. theorem OAI.MUB6.Certificate.PairSemantics.sound147 line 667
  55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation148 line 697
  56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix148 line 703
  57. theorem OAI.MUB6.Certificate.PairSemantics.sound148 line 705
  58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation149 line 735
  59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix149 line 741
  60. theorem OAI.MUB6.Certificate.PairSemantics.sound149 line 743
  61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation150 line 773
  62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix150 line 779
  63. theorem OAI.MUB6.Certificate.PairSemantics.sound150 line 781
  64. theorem OAI.MUB6.Certificate.PairSemantics.sound151 line 811
  65. theorem OAI.MUB6.Certificate.PairSemantics.sound152 line 816
  66. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation153 line 821
  67. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix153 line 827
  68. theorem OAI.MUB6.Certificate.PairSemantics.sound153 line 829
  69. theorem OAI.MUB6.Certificate.PairSemantics.sound154 line 859
  70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation155 line 864
  71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix155 line 870
  72. theorem OAI.MUB6.Certificate.PairSemantics.sound155 line 872
  73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation156 line 902
  74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix156 line 908
  75. theorem OAI.MUB6.Certificate.PairSemantics.sound156 line 910
  76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation157 line 940
  77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix157 line 946
  78. theorem OAI.MUB6.Certificate.PairSemantics.sound157 line 948
  79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation158 line 978
  80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix158 line 984
  81. theorem OAI.MUB6.Certificate.PairSemantics.sound158 line 986
  82. theorem OAI.MUB6.Certificate.PairSemantics.sound159 line 1016
  83. theorem OAI.MUB6.Certificate.PairSemantics.sound160 line 1021
  84. theorem OAI.MUB6.Certificate.PairSemantics.sound161 line 1026
  85. theorem OAI.MUB6.Certificate.PairSemantics.sound162 line 1031
  86. theorem OAI.MUB6.Certificate.PairSemantics.sound163 line 1036
  87. theorem OAI.MUB6.Certificate.PairSemantics.sound164 line 1041
  88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation165 line 1046
  89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix165 line 1052
  90. theorem OAI.MUB6.Certificate.PairSemantics.sound165 line 1054
  91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation166 line 1084
  92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix166 line 1090
  93. theorem OAI.MUB6.Certificate.PairSemantics.sound166 line 1092
  94. theorem OAI.MUB6.Certificate.PairSemantics.sound167 line 1122
  95. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation168 line 1127
  96. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix168 line 1133
  97. theorem OAI.MUB6.Certificate.PairSemantics.sound168 line 1135
  98. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation169 line 1165
  99. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix169 line 1171
  100. theorem OAI.MUB6.Certificate.PairSemantics.sound169 line 1173
  101. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation170 line 1203
  102. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix170 line 1209
  103. theorem OAI.MUB6.Certificate.PairSemantics.sound170 line 1211
  104. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation171 line 1241
  105. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix171 line 1247
  106. theorem OAI.MUB6.Certificate.PairSemantics.sound171 line 1249
  107. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation172 line 1279
  108. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix172 line 1285
  109. theorem OAI.MUB6.Certificate.PairSemantics.sound172 line 1287
  110. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation173 line 1317
  111. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix173 line 1323
  112. theorem OAI.MUB6.Certificate.PairSemantics.sound173 line 1325
  113. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation174 line 1355
  114. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix174 line 1361
  115. theorem OAI.MUB6.Certificate.PairSemantics.sound174 line 1363
  116. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation175 line 1393
  117. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix175 line 1399
  118. theorem OAI.MUB6.Certificate.PairSemantics.sound175 line 1401
  119. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation176 line 1431
  120. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix176 line 1437
  121. theorem OAI.MUB6.Certificate.PairSemantics.sound176 line 1439
  122. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation177 line 1469
  123. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix177 line 1475
  124. theorem OAI.MUB6.Certificate.PairSemantics.sound177 line 1477
  125. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation178 line 1507
  126. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix178 line 1513
  127. theorem OAI.MUB6.Certificate.PairSemantics.sound178 line 1515
  128. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation179 line 1545
  129. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix179 line 1551
  130. theorem OAI.MUB6.Certificate.PairSemantics.sound179 line 1553
  131. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation180 line 1583
  132. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix180 line 1589
  133. theorem OAI.MUB6.Certificate.PairSemantics.sound180 line 1591
  134. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation181 line 1621
  135. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix181 line 1627
  136. theorem OAI.MUB6.Certificate.PairSemantics.sound181 line 1629
  137. theorem OAI.MUB6.Certificate.PairSemantics.sound182 line 1659
  138. theorem OAI.MUB6.Certificate.PairSemantics.sound183 line 1664
  139. theorem OAI.MUB6.Certificate.PairSemantics.sound184 line 1669
  140. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation185 line 1674
  141. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix185 line 1680
  142. theorem OAI.MUB6.Certificate.PairSemantics.sound185 line 1682
  143. theorem OAI.MUB6.Certificate.PairSemantics.sound186 line 1712
  144. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation187 line 1717
  145. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix187 line 1723
  146. theorem OAI.MUB6.Certificate.PairSemantics.sound187 line 1725
  147. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation188 line 1755
  148. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix188 line 1761
  149. theorem OAI.MUB6.Certificate.PairSemantics.sound188 line 1763
  150. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation189 line 1793
  151. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix189 line 1799
  152. theorem OAI.MUB6.Certificate.PairSemantics.sound189 line 1801
  153. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation190 line 1831
  154. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix190 line 1837
  155. theorem OAI.MUB6.Certificate.PairSemantics.sound190 line 1839
  156. theorem OAI.MUB6.Certificate.PairSemantics.sound191 line 1869