OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound8.lean

GitHub source file

164 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.PairSemantics.sound512 line 47
2. theorem OAI.MUB6.Certificate.PairSemantics.sound513 line 52
3. theorem OAI.MUB6.Certificate.PairSemantics.sound514 line 57
4. theorem OAI.MUB6.Certificate.PairSemantics.sound515 line 62
5. theorem OAI.MUB6.Certificate.PairSemantics.sound516 line 67
6. theorem OAI.MUB6.Certificate.PairSemantics.sound517 line 72
7. theorem OAI.MUB6.Certificate.PairSemantics.sound518 line 77
8. theorem OAI.MUB6.Certificate.PairSemantics.sound519 line 82
9. theorem OAI.MUB6.Certificate.PairSemantics.sound520 line 87
10. theorem OAI.MUB6.Certificate.PairSemantics.sound521 line 92
11. theorem OAI.MUB6.Certificate.PairSemantics.sound522 line 97
12. theorem OAI.MUB6.Certificate.PairSemantics.sound523 line 102
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation524 line 107
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix524 line 113
15. theorem OAI.MUB6.Certificate.PairSemantics.sound524 line 115
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation525 line 150
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix525 line 156
18. theorem OAI.MUB6.Certificate.PairSemantics.sound525 line 158
19. theorem OAI.MUB6.Certificate.PairSemantics.sound526 line 193
20. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation527 line 198
21. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix527 line 204
22. theorem OAI.MUB6.Certificate.PairSemantics.sound527 line 206
23. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation528 line 241
24. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix528 line 247
25. theorem OAI.MUB6.Certificate.PairSemantics.sound528 line 249
26. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation529 line 284
27. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix529 line 290
28. theorem OAI.MUB6.Certificate.PairSemantics.sound529 line 292
29. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation530 line 327
30. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix530 line 333
31. theorem OAI.MUB6.Certificate.PairSemantics.sound530 line 335
32. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation531 line 370
33. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix531 line 376
34. theorem OAI.MUB6.Certificate.PairSemantics.sound531 line 378
35. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation532 line 413
36. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix532 line 419
37. theorem OAI.MUB6.Certificate.PairSemantics.sound532 line 421
38. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation533 line 456
39. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix533 line 462
40. theorem OAI.MUB6.Certificate.PairSemantics.sound533 line 464
41. theorem OAI.MUB6.Certificate.PairSemantics.sound534 line 499
42. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation535 line 504
43. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix535 line 510
44. theorem OAI.MUB6.Certificate.PairSemantics.sound535 line 512
45. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation536 line 547
46. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix536 line 553
47. theorem OAI.MUB6.Certificate.PairSemantics.sound536 line 555
48. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation537 line 590
49. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix537 line 596
50. theorem OAI.MUB6.Certificate.PairSemantics.sound537 line 598
51. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation538 line 633
52. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix538 line 639
53. theorem OAI.MUB6.Certificate.PairSemantics.sound538 line 641
54. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation539 line 676
55. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix539 line 682
56. theorem OAI.MUB6.Certificate.PairSemantics.sound539 line 684
57. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation540 line 719
58. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix540 line 725
59. theorem OAI.MUB6.Certificate.PairSemantics.sound540 line 727
60. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation541 line 762
61. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix541 line 768
62. theorem OAI.MUB6.Certificate.PairSemantics.sound541 line 770
63. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation542 line 805
64. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix542 line 811
65. theorem OAI.MUB6.Certificate.PairSemantics.sound542 line 813
66. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation543 line 848
67. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix543 line 854
68. theorem OAI.MUB6.Certificate.PairSemantics.sound543 line 856
69. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation544 line 891
70. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix544 line 897
71. theorem OAI.MUB6.Certificate.PairSemantics.sound544 line 899
72. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation545 line 934
73. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix545 line 940
74. theorem OAI.MUB6.Certificate.PairSemantics.sound545 line 942
75. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation546 line 977
76. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix546 line 983
77. theorem OAI.MUB6.Certificate.PairSemantics.sound546 line 985
78. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation547 line 1020
79. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix547 line 1026
80. theorem OAI.MUB6.Certificate.PairSemantics.sound547 line 1028
81. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation548 line 1063
82. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix548 line 1069
83. theorem OAI.MUB6.Certificate.PairSemantics.sound548 line 1071
84. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation549 line 1106
85. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix549 line 1112
86. theorem OAI.MUB6.Certificate.PairSemantics.sound549 line 1114
87. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation550 line 1149
88. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix550 line 1155
89. theorem OAI.MUB6.Certificate.PairSemantics.sound550 line 1157
90. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation551 line 1192
91. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix551 line 1198
92. theorem OAI.MUB6.Certificate.PairSemantics.sound551 line 1200
93. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation552 line 1235
94. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix552 line 1241
95. theorem OAI.MUB6.Certificate.PairSemantics.sound552 line 1243
96. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation553 line 1278
97. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix553 line 1284
98. theorem OAI.MUB6.Certificate.PairSemantics.sound553 line 1286
99. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation554 line 1321
100. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix554 line 1327
101. theorem OAI.MUB6.Certificate.PairSemantics.sound554 line 1329
102. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation555 line 1364
103. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix555 line 1370
104. theorem OAI.MUB6.Certificate.PairSemantics.sound555 line 1372
105. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation556 line 1407
106. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix556 line 1413
107. theorem OAI.MUB6.Certificate.PairSemantics.sound556 line 1415
108. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation557 line 1450
109. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix557 line 1456
110. theorem OAI.MUB6.Certificate.PairSemantics.sound557 line 1458
111. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation558 line 1493
112. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix558 line 1499
113. theorem OAI.MUB6.Certificate.PairSemantics.sound558 line 1501
114. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation559 line 1536
115. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix559 line 1542
116. theorem OAI.MUB6.Certificate.PairSemantics.sound559 line 1544
117. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation560 line 1579
118. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix560 line 1585
119. theorem OAI.MUB6.Certificate.PairSemantics.sound560 line 1587
120. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation561 line 1622
121. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix561 line 1628
122. theorem OAI.MUB6.Certificate.PairSemantics.sound561 line 1630
123. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation562 line 1665
124. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix562 line 1671
125. theorem OAI.MUB6.Certificate.PairSemantics.sound562 line 1673
126. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation563 line 1708
127. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix563 line 1714
128. theorem OAI.MUB6.Certificate.PairSemantics.sound563 line 1716
129. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation564 line 1751
130. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix564 line 1757
131. theorem OAI.MUB6.Certificate.PairSemantics.sound564 line 1759
132. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation565 line 1794
133. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix565 line 1800
134. theorem OAI.MUB6.Certificate.PairSemantics.sound565 line 1802
135. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation566 line 1837
136. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix566 line 1843
137. theorem OAI.MUB6.Certificate.PairSemantics.sound566 line 1845
138. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation567 line 1880
139. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix567 line 1886
140. theorem OAI.MUB6.Certificate.PairSemantics.sound567 line 1888
141. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation568 line 1923
142. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix568 line 1929
143. theorem OAI.MUB6.Certificate.PairSemantics.sound568 line 1931
144. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation569 line 1966
145. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix569 line 1972
146. theorem OAI.MUB6.Certificate.PairSemantics.sound569 line 1974
147. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation570 line 2009
148. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix570 line 2015
149. theorem OAI.MUB6.Certificate.PairSemantics.sound570 line 2017
150. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation571 line 2052
151. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix571 line 2058
152. theorem OAI.MUB6.Certificate.PairSemantics.sound571 line 2060
153. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation572 line 2095
154. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix572 line 2101
155. theorem OAI.MUB6.Certificate.PairSemantics.sound572 line 2103
156. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation573 line 2138
157. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix573 line 2144
158. theorem OAI.MUB6.Certificate.PairSemantics.sound573 line 2146
159. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation574 line 2181
160. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix574 line 2187
161. theorem OAI.MUB6.Certificate.PairSemantics.sound574 line 2189
162. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation575 line 2224
163. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix575 line 2230
164. theorem OAI.MUB6.Certificate.PairSemantics.sound575 line 2232