OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound3.lean

GitHub source file

156 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.PairSemantics.sound192 line 43
  2. theorem OAI.MUB6.Certificate.PairSemantics.sound193 line 48
  3. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation194 line 53
  4. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix194 line 59
  5. theorem OAI.MUB6.Certificate.PairSemantics.sound194 line 61
  6. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation195 line 91
  7. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix195 line 97
  8. theorem OAI.MUB6.Certificate.PairSemantics.sound195 line 99
  9. theorem OAI.MUB6.Certificate.PairSemantics.sound196 line 129
  10. theorem OAI.MUB6.Certificate.PairSemantics.sound197 line 134
  11. theorem OAI.MUB6.Certificate.PairSemantics.sound198 line 139
  12. theorem OAI.MUB6.Certificate.PairSemantics.sound199 line 144
  13. theorem OAI.MUB6.Certificate.PairSemantics.sound200 line 149
  14. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation201 line 154
  15. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix201 line 160
  16. theorem OAI.MUB6.Certificate.PairSemantics.sound201 line 162
  17. theorem OAI.MUB6.Certificate.PairSemantics.sound202 line 192
  18. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation203 line 197
  19. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix203 line 203
  20. theorem OAI.MUB6.Certificate.PairSemantics.sound203 line 205
  21. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation204 line 235
  22. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix204 line 241
  23. theorem OAI.MUB6.Certificate.PairSemantics.sound204 line 243
  24. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation205 line 273
  25. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix205 line 279
  26. theorem OAI.MUB6.Certificate.PairSemantics.sound205 line 281
  27. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation206 line 311
  28. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix206 line 317
  29. theorem OAI.MUB6.Certificate.PairSemantics.sound206 line 319
  30. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation207 line 349
  31. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix207 line 355
  32. theorem OAI.MUB6.Certificate.PairSemantics.sound207 line 357
  33. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation208 line 387
  34. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix208 line 393
  35. theorem OAI.MUB6.Certificate.PairSemantics.sound208 line 395
  36. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation209 line 425
  37. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix209 line 431
  38. theorem OAI.MUB6.Certificate.PairSemantics.sound209 line 433
  39. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation210 line 463
  40. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix210 line 469
  41. theorem OAI.MUB6.Certificate.PairSemantics.sound210 line 471
  42. theorem OAI.MUB6.Certificate.PairSemantics.sound211 line 501
  43. theorem OAI.MUB6.Certificate.PairSemantics.sound212 line 506
  44. theorem OAI.MUB6.Certificate.PairSemantics.sound213 line 511
  45. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation214 line 516
  46. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix214 line 522
  47. theorem OAI.MUB6.Certificate.PairSemantics.sound214 line 524
  48. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation215 line 554
  49. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix215 line 560
  50. theorem OAI.MUB6.Certificate.PairSemantics.sound215 line 562
  51. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation216 line 592
  52. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix216 line 598
  53. theorem OAI.MUB6.Certificate.PairSemantics.sound216 line 600
  54. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation217 line 630
  55. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix217 line 636
  56. theorem OAI.MUB6.Certificate.PairSemantics.sound217 line 638
  57. theorem OAI.MUB6.Certificate.PairSemantics.sound218 line 668
  58. theorem OAI.MUB6.Certificate.PairSemantics.sound219 line 673
  59. theorem OAI.MUB6.Certificate.PairSemantics.sound220 line 678
  60. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation221 line 683
  61. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix221 line 689
  62. theorem OAI.MUB6.Certificate.PairSemantics.sound221 line 691
  63. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation222 line 721
  64. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix222 line 727
  65. theorem OAI.MUB6.Certificate.PairSemantics.sound222 line 729
  66. theorem OAI.MUB6.Certificate.PairSemantics.sound223 line 759
  67. theorem OAI.MUB6.Certificate.PairSemantics.sound224 line 764
  68. theorem OAI.MUB6.Certificate.PairSemantics.sound225 line 769
  69. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation226 line 774
  70. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix226 line 780
  71. theorem OAI.MUB6.Certificate.PairSemantics.sound226 line 782
  72. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation227 line 812
  73. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix227 line 818
  74. theorem OAI.MUB6.Certificate.PairSemantics.sound227 line 820
  75. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation228 line 850
  76. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix228 line 856
  77. theorem OAI.MUB6.Certificate.PairSemantics.sound228 line 858
  78. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation229 line 888
  79. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix229 line 894
  80. theorem OAI.MUB6.Certificate.PairSemantics.sound229 line 896
  81. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation230 line 926
  82. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix230 line 932
  83. theorem OAI.MUB6.Certificate.PairSemantics.sound230 line 934
  84. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation231 line 964
  85. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix231 line 970
  86. theorem OAI.MUB6.Certificate.PairSemantics.sound231 line 972
  87. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation232 line 1007
  88. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix232 line 1013
  89. theorem OAI.MUB6.Certificate.PairSemantics.sound232 line 1015
  90. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation233 line 1050
  91. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix233 line 1056
  92. theorem OAI.MUB6.Certificate.PairSemantics.sound233 line 1058
  93. theorem OAI.MUB6.Certificate.PairSemantics.sound234 line 1088
  94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation235 line 1093
  95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix235 line 1099
  96. theorem OAI.MUB6.Certificate.PairSemantics.sound235 line 1101
  97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation236 line 1131
  98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix236 line 1137
  99. theorem OAI.MUB6.Certificate.PairSemantics.sound236 line 1139
  100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation237 line 1169
  101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix237 line 1175
  102. theorem OAI.MUB6.Certificate.PairSemantics.sound237 line 1177
  103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation238 line 1207
  104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix238 line 1213
  105. theorem OAI.MUB6.Certificate.PairSemantics.sound238 line 1215
  106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation239 line 1245
  107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix239 line 1251
  108. theorem OAI.MUB6.Certificate.PairSemantics.sound239 line 1253
  109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation240 line 1283
  110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix240 line 1289
  111. theorem OAI.MUB6.Certificate.PairSemantics.sound240 line 1291
  112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation241 line 1321
  113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix241 line 1327
  114. theorem OAI.MUB6.Certificate.PairSemantics.sound241 line 1329
  115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation242 line 1359
  116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix242 line 1365
  117. theorem OAI.MUB6.Certificate.PairSemantics.sound242 line 1367
  118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation243 line 1397
  119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix243 line 1403
  120. theorem OAI.MUB6.Certificate.PairSemantics.sound243 line 1405
  121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation244 line 1435
  122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix244 line 1441
  123. theorem OAI.MUB6.Certificate.PairSemantics.sound244 line 1443
  124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation245 line 1473
  125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix245 line 1479
  126. theorem OAI.MUB6.Certificate.PairSemantics.sound245 line 1481
  127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation246 line 1511
  128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix246 line 1517
  129. theorem OAI.MUB6.Certificate.PairSemantics.sound246 line 1519
  130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation247 line 1549
  131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix247 line 1555
  132. theorem OAI.MUB6.Certificate.PairSemantics.sound247 line 1557
  133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation248 line 1587
  134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix248 line 1593
  135. theorem OAI.MUB6.Certificate.PairSemantics.sound248 line 1595
  136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation249 line 1625
  137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix249 line 1631
  138. theorem OAI.MUB6.Certificate.PairSemantics.sound249 line 1633
  139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation250 line 1663
  140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix250 line 1669
  141. theorem OAI.MUB6.Certificate.PairSemantics.sound250 line 1671
  142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation251 line 1701
  143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix251 line 1707
  144. theorem OAI.MUB6.Certificate.PairSemantics.sound251 line 1709
  145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation252 line 1739
  146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix252 line 1745
  147. theorem OAI.MUB6.Certificate.PairSemantics.sound252 line 1747
  148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation253 line 1777
  149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix253 line 1783
  150. theorem OAI.MUB6.Certificate.PairSemantics.sound253 line 1785
  151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation254 line 1815
  152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix254 line 1821
  153. theorem OAI.MUB6.Certificate.PairSemantics.sound254 line 1823
  154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation255 line 1853
  155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix255 line 1859
  156. theorem OAI.MUB6.Certificate.PairSemantics.sound255 line 1861