OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound35.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2240 line 84
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2240 line 90
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2240 line 92
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2241 line 127
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2241 line 133
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2241 line 135
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2242 line 170
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2242 line 176
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2242 line 178
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2243 line 213
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2243 line 219
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2243 line 221
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2244 line 256
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2244 line 262
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2244 line 264
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2245 line 299
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2245 line 305
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2245 line 307
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2246 line 342
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2246 line 348
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2246 line 350
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2247 line 385
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2247 line 391
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2247 line 393
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2248 line 428
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2248 line 434
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2248 line 436
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2249 line 471
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2249 line 477
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2249 line 479
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2250 line 514
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2250 line 520
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2250 line 522
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2251 line 557
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2251 line 563
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2251 line 565
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2252 line 600
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2252 line 606
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2252 line 608
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2253 line 643
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2253 line 649
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2253 line 651
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2254 line 686
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2254 line 692
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2254 line 694
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2255 line 729
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2255 line 735
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2255 line 737
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2256 line 772
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2256 line 778
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2256 line 780
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2257 line 815
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2257 line 821
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2257 line 823
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2258 line 858
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2258 line 864
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2258 line 866
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2259 line 901
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2259 line 907
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2259 line 909
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2260 line 944
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2260 line 950
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2260 line 952
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2261 line 987
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2261 line 993
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2261 line 995
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2262 line 1030
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2262 line 1036
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2262 line 1038
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2263 line 1073
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2263 line 1079
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2263 line 1081
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2264 line 1116
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2264 line 1122
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2264 line 1124
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2265 line 1159
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2265 line 1165
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2265 line 1167
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2266 line 1202
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2266 line 1208
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2266 line 1210
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2267 line 1245
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2267 line 1251
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2267 line 1253
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2268 line 1288
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2268 line 1294
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2268 line 1296
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2269 line 1331
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2269 line 1337
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2269 line 1339
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2270 line 1374
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2270 line 1380
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2270 line 1382
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2271 line 1417
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2271 line 1423
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2271 line 1425
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2272 line 1460
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2272 line 1466
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2272 line 1468
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2273 line 1503
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2273 line 1509
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2273 line 1511
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2274 line 1546
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2274 line 1552
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2274 line 1554
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2275 line 1589
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2275 line 1595
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2275 line 1597
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2276 line 1632
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2276 line 1638
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2276 line 1640
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2277 line 1675
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2277 line 1681
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2277 line 1683
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2278 line 1718
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2278 line 1724
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2278 line 1726
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2279 line 1761
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2279 line 1767
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2279 line 1769
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2280 line 1804
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2280 line 1810
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2280 line 1812
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2281 line 1847
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2281 line 1853
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2281 line 1855
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2282 line 1890
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2282 line 1896
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2282 line 1898
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2283 line 1933
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2283 line 1939
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2283 line 1941
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2284 line 1976
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2284 line 1982
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2284 line 1984
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2285 line 2019
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2285 line 2025
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2285 line 2027
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2286 line 2062
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2286 line 2068
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2286 line 2070
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2287 line 2105
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2287 line 2111
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2287 line 2113
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2288 line 2148
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2288 line 2154
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2288 line 2156
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2289 line 2191
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2289 line 2197
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2289 line 2199
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2290 line 2234
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2290 line 2240
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2290 line 2242
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2291 line 2277
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2291 line 2283
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2291 line 2285
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2292 line 2320
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2292 line 2326
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2292 line 2328
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2293 line 2363
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2293 line 2369
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2293 line 2371
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2294 line 2406
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2294 line 2412
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2294 line 2414
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2295 line 2454
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2295 line 2460
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2295 line 2462
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2296 line 2502
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2296 line 2508
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2296 line 2510
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2297 line 2550
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2297 line 2556
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2297 line 2558
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2298 line 2598
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2298 line 2604
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2298 line 2606
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2299 line 2646
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2299 line 2652
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2299 line 2654
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2300 line 2694
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2300 line 2700
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2300 line 2702
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2301 line 2742
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2301 line 2748
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2301 line 2750
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2302 line 2790
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2302 line 2796
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2302 line 2798
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2303 line 2838
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2303 line 2844
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2303 line 2846