OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound23.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1472 line 80
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1472 line 86
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1472 line 88
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1473 line 123
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1473 line 129
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1473 line 131
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1474 line 166
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1474 line 172
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1474 line 174
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1475 line 209
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1475 line 215
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1475 line 217
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1476 line 252
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1476 line 258
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1476 line 260
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1477 line 295
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1477 line 301
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1477 line 303
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1478 line 338
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1478 line 344
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1478 line 346
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1479 line 381
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1479 line 387
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1479 line 389
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1480 line 424
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1480 line 430
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1480 line 432
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1481 line 467
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1481 line 473
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1481 line 475
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1482 line 510
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1482 line 516
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1482 line 518
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1483 line 553
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1483 line 559
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1483 line 561
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1484 line 596
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1484 line 602
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1484 line 604
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1485 line 639
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1485 line 645
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1485 line 647
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1486 line 682
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1486 line 688
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1486 line 690
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1487 line 725
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1487 line 731
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1487 line 733
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1488 line 768
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1488 line 774
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1488 line 776
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1489 line 811
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1489 line 817
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1489 line 819
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1490 line 854
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1490 line 860
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1490 line 862
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1491 line 897
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1491 line 903
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1491 line 905
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1492 line 940
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1492 line 946
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1492 line 948
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1493 line 983
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1493 line 989
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1493 line 991
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1494 line 1026
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1494 line 1032
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1494 line 1034
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1495 line 1069
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1495 line 1075
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1495 line 1077
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1496 line 1112
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1496 line 1118
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1496 line 1120
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1497 line 1155
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1497 line 1161
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1497 line 1163
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1498 line 1198
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1498 line 1204
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1498 line 1206
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1499 line 1241
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1499 line 1247
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1499 line 1249
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1500 line 1284
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1500 line 1290
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1500 line 1292
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1501 line 1327
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1501 line 1333
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1501 line 1335
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1502 line 1370
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1502 line 1376
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1502 line 1378
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1503 line 1413
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1503 line 1419
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1503 line 1421
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1504 line 1456
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1504 line 1462
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1504 line 1464
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1505 line 1499
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1505 line 1505
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1505 line 1507
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1506 line 1542
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1506 line 1548
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1506 line 1550
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1507 line 1585
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1507 line 1591
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1507 line 1593
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1508 line 1628
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1508 line 1634
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1508 line 1636
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1509 line 1671
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1509 line 1677
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1509 line 1679
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1510 line 1714
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1510 line 1720
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1510 line 1722
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1511 line 1757
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1511 line 1763
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1511 line 1765
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1512 line 1800
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1512 line 1806
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1512 line 1808
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1513 line 1843
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1513 line 1849
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1513 line 1851
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1514 line 1886
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1514 line 1892
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1514 line 1894
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1515 line 1929
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1515 line 1935
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1515 line 1937
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1516 line 1972
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1516 line 1978
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1516 line 1980
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1517 line 2015
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1517 line 2021
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1517 line 2023
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1518 line 2058
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1518 line 2064
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1518 line 2066
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1519 line 2101
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1519 line 2107
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1519 line 2109
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1520 line 2144
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1520 line 2150
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1520 line 2152
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1521 line 2187
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1521 line 2193
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1521 line 2195
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1522 line 2230
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1522 line 2236
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1522 line 2238
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1523 line 2273
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1523 line 2279
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1523 line 2281
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1524 line 2316
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1524 line 2322
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1524 line 2324
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1525 line 2359
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1525 line 2365
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1525 line 2367
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1526 line 2402
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1526 line 2408
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1526 line 2410
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1527 line 2450
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1527 line 2456
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1527 line 2458
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1528 line 2498
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1528 line 2504
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1528 line 2506
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1529 line 2546
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1529 line 2552
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1529 line 2554
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1530 line 2594
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1530 line 2600
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1530 line 2602
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1531 line 2642
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1531 line 2648
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1531 line 2650
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1532 line 2690
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1532 line 2696
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1532 line 2698
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1533 line 2738
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1533 line 2744
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1533 line 2746
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1534 line 2786
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1534 line 2792
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1534 line 2794
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1535 line 2834
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1535 line 2840
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1535 line 2842