OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound21.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1344 line 76
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1344 line 82
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1344 line 84
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1345 line 115
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1345 line 121
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1345 line 123
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1346 line 153
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1346 line 159
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1346 line 161
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1347 line 192
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1347 line 198
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1347 line 200
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1348 line 231
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1348 line 237
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1348 line 239
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1349 line 270
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1349 line 276
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1349 line 278
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1350 line 308
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1350 line 314
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1350 line 316
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1351 line 346
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1351 line 352
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1351 line 354
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1352 line 385
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1352 line 391
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1352 line 393
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1353 line 424
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1353 line 430
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1353 line 432
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1354 line 463
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1354 line 469
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1354 line 471
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1355 line 501
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1355 line 507
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1355 line 509
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1356 line 539
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1356 line 545
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1356 line 547
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1357 line 577
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1357 line 583
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1357 line 585
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1358 line 615
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1358 line 621
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1358 line 623
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1359 line 654
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1359 line 660
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1359 line 662
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1360 line 693
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1360 line 699
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1360 line 701
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1361 line 732
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1361 line 738
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1361 line 740
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1362 line 771
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1362 line 777
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1362 line 779
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1363 line 809
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1363 line 815
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1363 line 817
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1364 line 847
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1364 line 853
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1364 line 855
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1365 line 886
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1365 line 892
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1365 line 894
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1366 line 925
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1366 line 931
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1366 line 933
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1367 line 964
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1367 line 970
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1367 line 972
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1368 line 1002
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1368 line 1008
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1368 line 1010
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1369 line 1041
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1369 line 1047
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1369 line 1049
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1370 line 1080
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1370 line 1086
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1370 line 1088
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1371 line 1119
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1371 line 1125
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1371 line 1127
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1372 line 1157
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1372 line 1163
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1372 line 1165
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1373 line 1196
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1373 line 1202
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1373 line 1204
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1374 line 1235
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1374 line 1241
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1374 line 1243
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1375 line 1274
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1375 line 1280
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1375 line 1282
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1376 line 1313
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1376 line 1319
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1376 line 1321
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1377 line 1352
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1377 line 1358
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1377 line 1360
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1378 line 1391
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1378 line 1397
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1378 line 1399
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1379 line 1429
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1379 line 1435
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1379 line 1437
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1380 line 1477
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1380 line 1483
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1380 line 1485
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1381 line 1525
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1381 line 1531
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1381 line 1533
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1382 line 1573
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1382 line 1579
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1382 line 1581
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1383 line 1621
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1383 line 1627
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1383 line 1629
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1384 line 1669
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1384 line 1675
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1384 line 1677
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1385 line 1717
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1385 line 1723
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1385 line 1725
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1386 line 1765
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1386 line 1771
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1386 line 1773
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1387 line 1813
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1387 line 1819
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1387 line 1821
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1388 line 1861
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1388 line 1867
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1388 line 1869
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1389 line 1909
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1389 line 1915
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1389 line 1917
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1390 line 1957
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1390 line 1963
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1390 line 1965
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1391 line 2005
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1391 line 2011
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1391 line 2013
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1392 line 2053
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1392 line 2059
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1392 line 2061
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1393 line 2101
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1393 line 2107
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1393 line 2109
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1394 line 2149
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1394 line 2155
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1394 line 2157
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1395 line 2197
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1395 line 2203
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1395 line 2205
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1396 line 2245
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1396 line 2251
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1396 line 2253
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1397 line 2293
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1397 line 2299
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1397 line 2301
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1398 line 2341
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1398 line 2347
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1398 line 2349
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1399 line 2389
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1399 line 2395
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1399 line 2397
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1400 line 2437
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1400 line 2443
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1400 line 2445
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1401 line 2485
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1401 line 2491
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1401 line 2493
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1402 line 2533
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1402 line 2539
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1402 line 2541
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1403 line 2581
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1403 line 2587
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1403 line 2589
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1404 line 2629
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1404 line 2635
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1404 line 2637
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1405 line 2677
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1405 line 2683
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1405 line 2685
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1406 line 2725
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1406 line 2731
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1406 line 2733
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1407 line 2773
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1407 line 2779
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1407 line 2781