OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound22.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1408 line 73
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1408 line 79
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1408 line 81
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1409 line 121
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1409 line 127
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1409 line 129
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1410 line 169
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1410 line 175
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1410 line 177
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1411 line 217
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1411 line 223
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1411 line 225
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1412 line 265
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1412 line 271
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1412 line 273
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1413 line 313
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1413 line 319
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1413 line 321
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1414 line 361
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1414 line 367
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1414 line 369
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1415 line 409
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1415 line 415
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1415 line 417
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1416 line 457
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1416 line 463
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1416 line 465
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1417 line 505
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1417 line 511
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1417 line 513
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1418 line 553
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1418 line 559
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1418 line 561
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1419 line 601
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1419 line 607
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1419 line 609
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1420 line 649
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1420 line 655
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1420 line 657
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1421 line 697
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1421 line 703
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1421 line 705
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1422 line 745
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1422 line 751
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1422 line 753
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1423 line 793
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1423 line 799
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1423 line 801
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1424 line 841
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1424 line 847
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1424 line 849
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1425 line 889
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1425 line 895
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1425 line 897
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1426 line 937
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1426 line 943
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1426 line 945
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1427 line 985
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1427 line 991
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1427 line 993
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1428 line 1033
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1428 line 1039
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1428 line 1041
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1429 line 1081
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1429 line 1087
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1429 line 1089
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1430 line 1129
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1430 line 1135
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1430 line 1137
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1431 line 1177
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1431 line 1183
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1431 line 1185
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1432 line 1225
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1432 line 1231
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1432 line 1233
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1433 line 1273
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1433 line 1279
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1433 line 1281
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1434 line 1321
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1434 line 1327
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1434 line 1329
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1435 line 1369
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1435 line 1375
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1435 line 1377
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1436 line 1417
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1436 line 1423
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1436 line 1425
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1437 line 1465
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1437 line 1471
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1437 line 1473
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1438 line 1513
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1438 line 1519
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1438 line 1521
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1439 line 1561
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1439 line 1567
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1439 line 1569
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1440 line 1604
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1440 line 1610
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1440 line 1612
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1441 line 1647
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1441 line 1653
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1441 line 1655
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1442 line 1690
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1442 line 1696
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1442 line 1698
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1443 line 1733
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1443 line 1739
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1443 line 1741
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1444 line 1776
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1444 line 1782
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1444 line 1784
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1445 line 1819
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1445 line 1825
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1445 line 1827
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1446 line 1862
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1446 line 1868
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1446 line 1870
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1447 line 1905
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1447 line 1911
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1447 line 1913
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1448 line 1948
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1448 line 1954
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1448 line 1956
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1449 line 1991
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1449 line 1997
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1449 line 1999
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1450 line 2034
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1450 line 2040
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1450 line 2042
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1451 line 2077
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1451 line 2083
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1451 line 2085
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1452 line 2120
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1452 line 2126
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1452 line 2128
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1453 line 2163
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1453 line 2169
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1453 line 2171
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1454 line 2206
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1454 line 2212
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1454 line 2214
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1455 line 2249
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1455 line 2255
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1455 line 2257
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1456 line 2292
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1456 line 2298
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1456 line 2300
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1457 line 2335
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1457 line 2341
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1457 line 2343
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1458 line 2378
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1458 line 2384
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1458 line 2386
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1459 line 2421
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1459 line 2427
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1459 line 2429
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1460 line 2464
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1460 line 2470
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1460 line 2472
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1461 line 2507
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1461 line 2513
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1461 line 2515
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1462 line 2550
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1462 line 2556
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1462 line 2558
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1463 line 2593
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1463 line 2599
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1463 line 2601
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1464 line 2636
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1464 line 2642
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1464 line 2644
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1465 line 2679
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1465 line 2685
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1465 line 2687
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1466 line 2722
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1466 line 2728
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1466 line 2730
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1467 line 2765
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1467 line 2771
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1467 line 2773
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1468 line 2808
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1468 line 2814
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1468 line 2816
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1469 line 2851
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1469 line 2857
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1469 line 2859
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1470 line 2894
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1470 line 2900
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1470 line 2902
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1471 line 2937
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1471 line 2943
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1471 line 2945