OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound24.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1536 line 76
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1536 line 82
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1536 line 84
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1537 line 124
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1537 line 130
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1537 line 132
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1538 line 172
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1538 line 178
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1538 line 180
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1539 line 220
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1539 line 226
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1539 line 228
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1540 line 268
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1540 line 274
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1540 line 276
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1541 line 316
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1541 line 322
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1541 line 324
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1542 line 364
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1542 line 370
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1542 line 372
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1543 line 412
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1543 line 418
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1543 line 420
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1544 line 460
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1544 line 466
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1544 line 468
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1545 line 503
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1545 line 509
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1545 line 511
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1546 line 546
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1546 line 552
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1546 line 554
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1547 line 589
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1547 line 595
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1547 line 597
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1548 line 632
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1548 line 638
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1548 line 640
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1549 line 675
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1549 line 681
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1549 line 683
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1550 line 718
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1550 line 724
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1550 line 726
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1551 line 761
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1551 line 767
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1551 line 769
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1552 line 804
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1552 line 810
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1552 line 812
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1553 line 847
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1553 line 853
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1553 line 855
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1554 line 890
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1554 line 896
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1554 line 898
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1555 line 933
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1555 line 939
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1555 line 941
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1556 line 976
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1556 line 982
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1556 line 984
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1557 line 1019
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1557 line 1025
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1557 line 1027
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1558 line 1062
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1558 line 1068
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1558 line 1070
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1559 line 1105
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1559 line 1111
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1559 line 1113
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1560 line 1148
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1560 line 1154
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1560 line 1156
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1561 line 1191
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1561 line 1197
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1561 line 1199
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1562 line 1234
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1562 line 1240
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1562 line 1242
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1563 line 1277
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1563 line 1283
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1563 line 1285
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1564 line 1320
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1564 line 1326
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1564 line 1328
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1565 line 1363
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1565 line 1369
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1565 line 1371
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1566 line 1406
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1566 line 1412
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1566 line 1414
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1567 line 1449
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1567 line 1455
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1567 line 1457
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1568 line 1492
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1568 line 1498
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1568 line 1500
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1569 line 1535
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1569 line 1541
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1569 line 1543
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1570 line 1578
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1570 line 1584
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1570 line 1586
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1571 line 1621
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1571 line 1627
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1571 line 1629
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1572 line 1664
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1572 line 1670
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1572 line 1672
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1573 line 1707
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1573 line 1713
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1573 line 1715
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1574 line 1750
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1574 line 1756
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1574 line 1758
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1575 line 1793
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1575 line 1799
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1575 line 1801
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1576 line 1836
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1576 line 1842
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1576 line 1844
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1577 line 1879
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1577 line 1885
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1577 line 1887
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1578 line 1922
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1578 line 1928
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1578 line 1930
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1579 line 1965
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1579 line 1971
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1579 line 1973
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1580 line 2008
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1580 line 2014
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1580 line 2016
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1581 line 2051
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1581 line 2057
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1581 line 2059
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1582 line 2094
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1582 line 2100
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1582 line 2102
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1583 line 2137
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1583 line 2143
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1583 line 2145
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1584 line 2180
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1584 line 2186
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1584 line 2188
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1585 line 2223
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1585 line 2229
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1585 line 2231
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1586 line 2266
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1586 line 2272
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1586 line 2274
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1587 line 2309
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1587 line 2315
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1587 line 2317
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1588 line 2352
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1588 line 2358
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1588 line 2360
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1589 line 2395
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1589 line 2401
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1589 line 2403
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1590 line 2438
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1590 line 2444
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1590 line 2446
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1591 line 2481
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1591 line 2487
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1591 line 2489
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1592 line 2524
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1592 line 2530
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1592 line 2532
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1593 line 2567
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1593 line 2573
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1593 line 2575
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1594 line 2610
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1594 line 2616
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1594 line 2618
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1595 line 2653
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1595 line 2659
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1595 line 2661
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1596 line 2696
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1596 line 2702
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1596 line 2704
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1597 line 2739
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1597 line 2745
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1597 line 2747
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1598 line 2782
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1598 line 2788
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1598 line 2790
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1599 line 2825
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1599 line 2831
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1599 line 2833