OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound6.lean

GitHub source file

144 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation384 line 38
  2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix384 line 44
  3. theorem OAI.MUB6.Certificate.PairSemantics.sound384 line 46
  4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation385 line 81
  5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix385 line 87
  6. theorem OAI.MUB6.Certificate.PairSemantics.sound385 line 89
  7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation386 line 124
  8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix386 line 130
  9. theorem OAI.MUB6.Certificate.PairSemantics.sound386 line 132
  10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation387 line 167
  11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix387 line 173
  12. theorem OAI.MUB6.Certificate.PairSemantics.sound387 line 175
  13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation388 line 210
  14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix388 line 216
  15. theorem OAI.MUB6.Certificate.PairSemantics.sound388 line 218
  16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation389 line 253
  17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix389 line 259
  18. theorem OAI.MUB6.Certificate.PairSemantics.sound389 line 261
  19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation390 line 296
  20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix390 line 302
  21. theorem OAI.MUB6.Certificate.PairSemantics.sound390 line 304
  22. theorem OAI.MUB6.Certificate.PairSemantics.sound391 line 339
  23. theorem OAI.MUB6.Certificate.PairSemantics.sound392 line 344
  24. theorem OAI.MUB6.Certificate.PairSemantics.sound393 line 349
  25. theorem OAI.MUB6.Certificate.PairSemantics.sound394 line 354
  26. theorem OAI.MUB6.Certificate.PairSemantics.sound395 line 359
  27. theorem OAI.MUB6.Certificate.PairSemantics.sound396 line 364
  28. theorem OAI.MUB6.Certificate.PairSemantics.sound397 line 369
  29. theorem OAI.MUB6.Certificate.PairSemantics.sound398 line 374
  30. theorem OAI.MUB6.Certificate.PairSemantics.sound399 line 379
  31. theorem OAI.MUB6.Certificate.PairSemantics.sound400 line 384
  32. theorem OAI.MUB6.Certificate.PairSemantics.sound401 line 389
  33. theorem OAI.MUB6.Certificate.PairSemantics.sound402 line 394
  34. theorem OAI.MUB6.Certificate.PairSemantics.sound403 line 399
  35. theorem OAI.MUB6.Certificate.PairSemantics.sound404 line 404
  36. theorem OAI.MUB6.Certificate.PairSemantics.sound405 line 409
  37. theorem OAI.MUB6.Certificate.PairSemantics.sound406 line 414
  38. theorem OAI.MUB6.Certificate.PairSemantics.sound407 line 419
  39. theorem OAI.MUB6.Certificate.PairSemantics.sound408 line 424
  40. theorem OAI.MUB6.Certificate.PairSemantics.sound409 line 429
  41. theorem OAI.MUB6.Certificate.PairSemantics.sound410 line 434
  42. theorem OAI.MUB6.Certificate.PairSemantics.sound411 line 439
  43. theorem OAI.MUB6.Certificate.PairSemantics.sound412 line 444
  44. theorem OAI.MUB6.Certificate.PairSemantics.sound413 line 449
  45. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation414 line 454
  46. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix414 line 460
  47. theorem OAI.MUB6.Certificate.PairSemantics.sound414 line 462
  48. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation415 line 497
  49. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix415 line 503
  50. theorem OAI.MUB6.Certificate.PairSemantics.sound415 line 505
  51. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation416 line 540
  52. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix416 line 546
  53. theorem OAI.MUB6.Certificate.PairSemantics.sound416 line 548
  54. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation417 line 583
  55. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix417 line 589
  56. theorem OAI.MUB6.Certificate.PairSemantics.sound417 line 591
  57. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation418 line 626
  58. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix418 line 632
  59. theorem OAI.MUB6.Certificate.PairSemantics.sound418 line 634
  60. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation419 line 669
  61. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix419 line 675
  62. theorem OAI.MUB6.Certificate.PairSemantics.sound419 line 677
  63. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation420 line 712
  64. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix420 line 718
  65. theorem OAI.MUB6.Certificate.PairSemantics.sound420 line 720
  66. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation421 line 755
  67. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix421 line 761
  68. theorem OAI.MUB6.Certificate.PairSemantics.sound421 line 763
  69. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation422 line 798
  70. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix422 line 804
  71. theorem OAI.MUB6.Certificate.PairSemantics.sound422 line 806
  72. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation423 line 841
  73. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix423 line 847
  74. theorem OAI.MUB6.Certificate.PairSemantics.sound423 line 849
  75. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation424 line 884
  76. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix424 line 890
  77. theorem OAI.MUB6.Certificate.PairSemantics.sound424 line 892
  78. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation425 line 927
  79. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix425 line 933
  80. theorem OAI.MUB6.Certificate.PairSemantics.sound425 line 935
  81. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation426 line 970
  82. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix426 line 976
  83. theorem OAI.MUB6.Certificate.PairSemantics.sound426 line 978
  84. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation427 line 1013
  85. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix427 line 1019
  86. theorem OAI.MUB6.Certificate.PairSemantics.sound427 line 1021
  87. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation428 line 1056
  88. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix428 line 1062
  89. theorem OAI.MUB6.Certificate.PairSemantics.sound428 line 1064
  90. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation429 line 1099
  91. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix429 line 1105
  92. theorem OAI.MUB6.Certificate.PairSemantics.sound429 line 1107
  93. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation430 line 1142
  94. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix430 line 1148
  95. theorem OAI.MUB6.Certificate.PairSemantics.sound430 line 1150
  96. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation431 line 1185
  97. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix431 line 1191
  98. theorem OAI.MUB6.Certificate.PairSemantics.sound431 line 1193
  99. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation432 line 1228
  100. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix432 line 1234
  101. theorem OAI.MUB6.Certificate.PairSemantics.sound432 line 1236
  102. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation433 line 1271
  103. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix433 line 1277
  104. theorem OAI.MUB6.Certificate.PairSemantics.sound433 line 1279
  105. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation434 line 1314
  106. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix434 line 1320
  107. theorem OAI.MUB6.Certificate.PairSemantics.sound434 line 1322
  108. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation435 line 1357
  109. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix435 line 1363
  110. theorem OAI.MUB6.Certificate.PairSemantics.sound435 line 1365
  111. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation436 line 1400
  112. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix436 line 1406
  113. theorem OAI.MUB6.Certificate.PairSemantics.sound436 line 1408
  114. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation437 line 1443
  115. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix437 line 1449
  116. theorem OAI.MUB6.Certificate.PairSemantics.sound437 line 1451
  117. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation438 line 1486
  118. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix438 line 1492
  119. theorem OAI.MUB6.Certificate.PairSemantics.sound438 line 1494
  120. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation439 line 1529
  121. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix439 line 1535
  122. theorem OAI.MUB6.Certificate.PairSemantics.sound439 line 1537
  123. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation440 line 1572
  124. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix440 line 1578
  125. theorem OAI.MUB6.Certificate.PairSemantics.sound440 line 1580
  126. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation441 line 1615
  127. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix441 line 1621
  128. theorem OAI.MUB6.Certificate.PairSemantics.sound441 line 1623
  129. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation442 line 1658
  130. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix442 line 1664
  131. theorem OAI.MUB6.Certificate.PairSemantics.sound442 line 1666
  132. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation443 line 1701
  133. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix443 line 1707
  134. theorem OAI.MUB6.Certificate.PairSemantics.sound443 line 1709
  135. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation444 line 1744
  136. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix444 line 1750
  137. theorem OAI.MUB6.Certificate.PairSemantics.sound444 line 1752
  138. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation445 line 1787
  139. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix445 line 1793
  140. theorem OAI.MUB6.Certificate.PairSemantics.sound445 line 1795
  141. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation446 line 1830
  142. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix446 line 1836
  143. theorem OAI.MUB6.Certificate.PairSemantics.sound446 line 1838
  144. theorem OAI.MUB6.Certificate.PairSemantics.sound447 line 1873