OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound18.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1152 line 64
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1152 line 70
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1152 line 72
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1153 line 107
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1153 line 113
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1153 line 115
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1154 line 150
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1154 line 156
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1154 line 158
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1155 line 189
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1155 line 195
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1155 line 197
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1156 line 228
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1156 line 234
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1156 line 236
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1157 line 266
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1157 line 272
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1157 line 274
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1158 line 305
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1158 line 311
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1158 line 313
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1159 line 344
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1159 line 350
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1159 line 352
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1160 line 383
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1160 line 389
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1160 line 391
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1161 line 422
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1161 line 428
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1161 line 430
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1162 line 461
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1162 line 467
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1162 line 469
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1163 line 500
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1163 line 506
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1163 line 508
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1164 line 539
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1164 line 545
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1164 line 547
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1165 line 578
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1165 line 584
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1165 line 586
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1166 line 616
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1166 line 622
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1166 line 624
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1167 line 655
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1167 line 661
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1167 line 663
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1168 line 693
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1168 line 699
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1168 line 701
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1169 line 731
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1169 line 737
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1169 line 739
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1170 line 769
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1170 line 775
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1170 line 777
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1171 line 807
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1171 line 813
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1171 line 815
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1172 line 845
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1172 line 851
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1172 line 853
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1173 line 884
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1173 line 890
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1173 line 892
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1174 line 923
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1174 line 929
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1174 line 931
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1175 line 961
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1175 line 967
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1175 line 969
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1176 line 999
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1176 line 1005
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1176 line 1007
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1177 line 1037
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1177 line 1043
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1177 line 1045
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1178 line 1075
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1178 line 1081
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1178 line 1083
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1179 line 1113
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1179 line 1119
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1179 line 1121
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1180 line 1152
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1180 line 1158
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1180 line 1160
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1181 line 1191
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1181 line 1197
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1181 line 1199
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1182 line 1229
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1182 line 1235
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1182 line 1237
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1183 line 1268
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1183 line 1274
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1183 line 1276
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1184 line 1307
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1184 line 1313
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1184 line 1315
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1185 line 1346
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1185 line 1352
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1185 line 1354
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1186 line 1384
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1186 line 1390
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1186 line 1392
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1187 line 1423
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1187 line 1429
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1187 line 1431
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1188 line 1462
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1188 line 1468
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1188 line 1470
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1189 line 1501
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1189 line 1507
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1189 line 1509
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1190 line 1539
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1190 line 1545
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1190 line 1547
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1191 line 1578
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1191 line 1584
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1191 line 1586
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1192 line 1616
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1192 line 1622
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1192 line 1624
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1193 line 1655
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1193 line 1661
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1193 line 1663
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1194 line 1693
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1194 line 1699
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1194 line 1701
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1195 line 1732
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1195 line 1738
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1195 line 1740
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1196 line 1771
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1196 line 1777
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1196 line 1779
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1197 line 1810
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1197 line 1816
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1197 line 1818
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1198 line 1848
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1198 line 1854
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1198 line 1856
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1199 line 1886
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1199 line 1892
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1199 line 1894
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1200 line 1924
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1200 line 1930
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1200 line 1932
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1201 line 1962
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1201 line 1968
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1201 line 1970
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1202 line 2000
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1202 line 2006
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1202 line 2008
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1203 line 2038
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1203 line 2044
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1203 line 2046
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1204 line 2076
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1204 line 2082
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1204 line 2084
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1205 line 2114
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1205 line 2120
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1205 line 2122
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1206 line 2153
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1206 line 2159
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1206 line 2161
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1207 line 2191
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1207 line 2197
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1207 line 2199
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1208 line 2229
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1208 line 2235
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1208 line 2237
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1209 line 2268
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1209 line 2274
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1209 line 2276
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1210 line 2307
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1210 line 2313
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1210 line 2315
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1211 line 2346
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1211 line 2352
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1211 line 2354
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1212 line 2384
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1212 line 2390
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1212 line 2392
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1213 line 2422
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1213 line 2428
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1213 line 2430
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1214 line 2461
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1214 line 2467
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1214 line 2469
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1215 line 2499
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1215 line 2505
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1215 line 2507