OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound20.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1280 line 81
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1280 line 87
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1280 line 89
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1281 line 119
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1281 line 125
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1281 line 127
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1282 line 157
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1282 line 163
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1282 line 165
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1283 line 195
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1283 line 201
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1283 line 203
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1284 line 233
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1284 line 239
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1284 line 241
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1285 line 271
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1285 line 277
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1285 line 279
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1286 line 309
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1286 line 315
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1286 line 317
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1287 line 347
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1287 line 353
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1287 line 355
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1288 line 390
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1288 line 396
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1288 line 398
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1289 line 433
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1289 line 439
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1289 line 441
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1290 line 476
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1290 line 482
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1290 line 484
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1291 line 519
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1291 line 525
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1291 line 527
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1292 line 562
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1292 line 568
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1292 line 570
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1293 line 605
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1293 line 611
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1293 line 613
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1294 line 648
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1294 line 654
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1294 line 656
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1295 line 691
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1295 line 697
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1295 line 699
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1296 line 729
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1296 line 735
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1296 line 737
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1297 line 767
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1297 line 773
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1297 line 775
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1298 line 805
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1298 line 811
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1298 line 813
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1299 line 843
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1299 line 849
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1299 line 851
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1300 line 881
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1300 line 887
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1300 line 889
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1301 line 919
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1301 line 925
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1301 line 927
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1302 line 957
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1302 line 963
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1302 line 965
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1303 line 995
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1303 line 1001
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1303 line 1003
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1304 line 1034
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1304 line 1040
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1304 line 1042
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1305 line 1073
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1305 line 1079
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1305 line 1081
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1306 line 1112
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1306 line 1118
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1306 line 1120
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1307 line 1151
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1307 line 1157
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1307 line 1159
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1308 line 1189
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1308 line 1195
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1308 line 1197
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1309 line 1228
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1309 line 1234
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1309 line 1236
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1310 line 1267
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1310 line 1273
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1310 line 1275
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1311 line 1306
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1311 line 1312
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1311 line 1314
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1312 line 1344
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1312 line 1350
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1312 line 1352
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1313 line 1382
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1313 line 1388
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1313 line 1390
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1314 line 1421
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1314 line 1427
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1314 line 1429
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1315 line 1460
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1315 line 1466
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1315 line 1468
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1316 line 1499
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1316 line 1505
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1316 line 1507
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1317 line 1537
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1317 line 1543
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1317 line 1545
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1318 line 1575
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1318 line 1581
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1318 line 1583
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1319 line 1614
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1319 line 1620
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1319 line 1622
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1320 line 1653
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1320 line 1659
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1320 line 1661
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1321 line 1691
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1321 line 1697
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1321 line 1699
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1322 line 1730
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1322 line 1736
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1322 line 1738
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1323 line 1769
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1323 line 1775
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1323 line 1777
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1324 line 1817
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1324 line 1823
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1324 line 1825
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1325 line 1856
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1325 line 1862
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1325 line 1864
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1326 line 1895
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1326 line 1901
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1326 line 1903
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1327 line 1933
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1327 line 1939
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1327 line 1941
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1328 line 1972
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1328 line 1978
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1328 line 1980
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1329 line 2010
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1329 line 2016
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1329 line 2018
151. theorem OAI.MUB6.Certificate.PairSemantics.sound1330 line 2049
152. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1331 line 2054
153. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1331 line 2060
154. theorem OAI.MUB6.Certificate.PairSemantics.sound1331 line 2062
155. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1332 line 2093
156. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1332 line 2099
157. theorem OAI.MUB6.Certificate.PairSemantics.sound1332 line 2101
158. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1333 line 2132
159. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1333 line 2138
160. theorem OAI.MUB6.Certificate.PairSemantics.sound1333 line 2140
161. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1334 line 2171
162. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1334 line 2177
163. theorem OAI.MUB6.Certificate.PairSemantics.sound1334 line 2179
164. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1335 line 2209
165. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1335 line 2215
166. theorem OAI.MUB6.Certificate.PairSemantics.sound1335 line 2217
167. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1336 line 2247
168. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1336 line 2253
169. theorem OAI.MUB6.Certificate.PairSemantics.sound1336 line 2255
170. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1337 line 2285
171. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1337 line 2291
172. theorem OAI.MUB6.Certificate.PairSemantics.sound1337 line 2293
173. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1338 line 2323
174. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1338 line 2329
175. theorem OAI.MUB6.Certificate.PairSemantics.sound1338 line 2331
176. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1339 line 2362
177. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1339 line 2368
178. theorem OAI.MUB6.Certificate.PairSemantics.sound1339 line 2370
179. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1340 line 2401
180. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1340 line 2407
181. theorem OAI.MUB6.Certificate.PairSemantics.sound1340 line 2409
182. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1341 line 2439
183. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1341 line 2445
184. theorem OAI.MUB6.Certificate.PairSemantics.sound1341 line 2447
185. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1342 line 2478
186. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1342 line 2484
187. theorem OAI.MUB6.Certificate.PairSemantics.sound1342 line 2486
188. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1343 line 2517
189. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1343 line 2523
190. theorem OAI.MUB6.Certificate.PairSemantics.sound1343 line 2525