OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound0.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.PairSemantics.sound0 line 31
  2. theorem OAI.MUB6.Certificate.PairSemantics.sound1 line 36
  3. theorem OAI.MUB6.Certificate.PairSemantics.sound2 line 41
  4. theorem OAI.MUB6.Certificate.PairSemantics.sound3 line 46
  5. theorem OAI.MUB6.Certificate.PairSemantics.sound4 line 51
  6. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation5 line 56
  7. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix5 line 62
  8. theorem OAI.MUB6.Certificate.PairSemantics.sound5 line 64
  9. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation6 line 84
  10. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix6 line 90
  11. theorem OAI.MUB6.Certificate.PairSemantics.sound6 line 92
  12. theorem OAI.MUB6.Certificate.PairSemantics.sound7 line 117
  13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation8 line 122
  14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix8 line 128
  15. theorem OAI.MUB6.Certificate.PairSemantics.sound8 line 130
  16. theorem OAI.MUB6.Certificate.PairSemantics.sound9 line 155
  17. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation10 line 160
  18. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix10 line 166
  19. theorem OAI.MUB6.Certificate.PairSemantics.sound10 line 168
  20. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation11 line 193
  21. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix11 line 199
  22. theorem OAI.MUB6.Certificate.PairSemantics.sound11 line 201
  23. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation12 line 226
  24. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix12 line 232
  25. theorem OAI.MUB6.Certificate.PairSemantics.sound12 line 234
  26. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation13 line 264
  27. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix13 line 270
  28. theorem OAI.MUB6.Certificate.PairSemantics.sound13 line 272
  29. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation14 line 302
  30. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix14 line 308
  31. theorem OAI.MUB6.Certificate.PairSemantics.sound14 line 310
  32. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation15 line 340
  33. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix15 line 346
  34. theorem OAI.MUB6.Certificate.PairSemantics.sound15 line 348
  35. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation16 line 378
  36. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix16 line 384
  37. theorem OAI.MUB6.Certificate.PairSemantics.sound16 line 386
  38. theorem OAI.MUB6.Certificate.PairSemantics.sound17 line 416
  39. theorem OAI.MUB6.Certificate.PairSemantics.sound18 line 421
  40. theorem OAI.MUB6.Certificate.PairSemantics.sound19 line 426
  41. theorem OAI.MUB6.Certificate.PairSemantics.sound20 line 431
  42. theorem OAI.MUB6.Certificate.PairSemantics.sound21 line 436
  43. theorem OAI.MUB6.Certificate.PairSemantics.sound22 line 441
  44. theorem OAI.MUB6.Certificate.PairSemantics.sound23 line 446
  45. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation24 line 451
  46. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix24 line 457
  47. theorem OAI.MUB6.Certificate.PairSemantics.sound24 line 459
  48. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation25 line 489
  49. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix25 line 495
  50. theorem OAI.MUB6.Certificate.PairSemantics.sound25 line 497
  51. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation26 line 527
  52. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix26 line 533
  53. theorem OAI.MUB6.Certificate.PairSemantics.sound26 line 535
  54. theorem OAI.MUB6.Certificate.PairSemantics.sound27 line 565
  55. theorem OAI.MUB6.Certificate.PairSemantics.sound28 line 570
  56. theorem OAI.MUB6.Certificate.PairSemantics.sound29 line 575
  57. theorem OAI.MUB6.Certificate.PairSemantics.sound30 line 580
  58. theorem OAI.MUB6.Certificate.PairSemantics.sound31 line 585
  59. theorem OAI.MUB6.Certificate.PairSemantics.sound32 line 590
  60. theorem OAI.MUB6.Certificate.PairSemantics.sound33 line 595
  61. theorem OAI.MUB6.Certificate.PairSemantics.sound34 line 600
  62. theorem OAI.MUB6.Certificate.PairSemantics.sound35 line 605
  63. theorem OAI.MUB6.Certificate.PairSemantics.sound36 line 610
  64. theorem OAI.MUB6.Certificate.PairSemantics.sound37 line 615
  65. theorem OAI.MUB6.Certificate.PairSemantics.sound38 line 620
  66. theorem OAI.MUB6.Certificate.PairSemantics.sound39 line 625
  67. theorem OAI.MUB6.Certificate.PairSemantics.sound40 line 630
  68. theorem OAI.MUB6.Certificate.PairSemantics.sound41 line 635
  69. theorem OAI.MUB6.Certificate.PairSemantics.sound42 line 640
  70. theorem OAI.MUB6.Certificate.PairSemantics.sound43 line 645
  71. theorem OAI.MUB6.Certificate.PairSemantics.sound44 line 650
  72. theorem OAI.MUB6.Certificate.PairSemantics.sound45 line 655
  73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation46 line 660
  74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix46 line 666
  75. theorem OAI.MUB6.Certificate.PairSemantics.sound46 line 668
  76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation47 line 698
  77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix47 line 704
  78. theorem OAI.MUB6.Certificate.PairSemantics.sound47 line 706
  79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation48 line 731
  80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix48 line 737
  81. theorem OAI.MUB6.Certificate.PairSemantics.sound48 line 739
  82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation49 line 765
  83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix49 line 771
  84. theorem OAI.MUB6.Certificate.PairSemantics.sound49 line 773
  85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation50 line 799
  86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix50 line 805
  87. theorem OAI.MUB6.Certificate.PairSemantics.sound50 line 807
  88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation51 line 832
  89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix51 line 838
  90. theorem OAI.MUB6.Certificate.PairSemantics.sound51 line 840
  91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation52 line 865
  92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix52 line 871
  93. theorem OAI.MUB6.Certificate.PairSemantics.sound52 line 873
  94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation53 line 899
  95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix53 line 905
  96. theorem OAI.MUB6.Certificate.PairSemantics.sound53 line 907
  97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation54 line 932
  98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix54 line 938
  99. theorem OAI.MUB6.Certificate.PairSemantics.sound54 line 940
  100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation55 line 965
  101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix55 line 971
  102. theorem OAI.MUB6.Certificate.PairSemantics.sound55 line 973
  103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation56 line 999
  104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix56 line 1005
  105. theorem OAI.MUB6.Certificate.PairSemantics.sound56 line 1007
  106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation57 line 1032
  107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix57 line 1038
  108. theorem OAI.MUB6.Certificate.PairSemantics.sound57 line 1040
  109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation58 line 1065
  110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix58 line 1071
  111. theorem OAI.MUB6.Certificate.PairSemantics.sound58 line 1073
  112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation59 line 1098
  113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix59 line 1104
  114. theorem OAI.MUB6.Certificate.PairSemantics.sound59 line 1106
  115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation60 line 1132
  116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix60 line 1138
  117. theorem OAI.MUB6.Certificate.PairSemantics.sound60 line 1140
  118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation61 line 1166
  119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix61 line 1172
  120. theorem OAI.MUB6.Certificate.PairSemantics.sound61 line 1174
  121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation62 line 1199
  122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix62 line 1205
  123. theorem OAI.MUB6.Certificate.PairSemantics.sound62 line 1207
  124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation63 line 1232
  125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix63 line 1238
  126. theorem OAI.MUB6.Certificate.PairSemantics.sound63 line 1240