OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound36.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2304 line 83
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2304 line 89
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2304 line 91
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2305 line 131
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2305 line 137
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2305 line 139
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2306 line 179
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2306 line 185
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2306 line 187
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2307 line 227
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2307 line 233
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2307 line 235
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2308 line 270
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2308 line 276
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2308 line 278
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2309 line 313
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2309 line 319
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2309 line 321
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2310 line 356
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2310 line 362
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2310 line 364
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2311 line 399
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2311 line 405
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2311 line 407
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2312 line 442
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2312 line 448
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2312 line 450
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2313 line 485
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2313 line 491
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2313 line 493
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2314 line 528
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2314 line 534
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2314 line 536
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2315 line 571
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2315 line 577
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2315 line 579
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2316 line 614
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2316 line 620
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2316 line 622
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2317 line 657
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2317 line 663
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2317 line 665
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2318 line 700
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2318 line 706
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2318 line 708
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2319 line 743
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2319 line 749
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2319 line 751
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2320 line 786
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2320 line 792
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2320 line 794
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2321 line 829
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2321 line 835
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2321 line 837
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2322 line 872
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2322 line 878
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2322 line 880
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2323 line 915
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2323 line 921
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2323 line 923
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2324 line 958
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2324 line 964
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2324 line 966
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2325 line 1001
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2325 line 1007
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2325 line 1009
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2326 line 1044
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2326 line 1050
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2326 line 1052
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2327 line 1087
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2327 line 1093
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2327 line 1095
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2328 line 1130
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2328 line 1136
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2328 line 1138
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2329 line 1173
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2329 line 1179
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2329 line 1181
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2330 line 1216
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2330 line 1222
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2330 line 1224
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2331 line 1259
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2331 line 1265
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2331 line 1267
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2332 line 1302
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2332 line 1308
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2332 line 1310
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2333 line 1345
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2333 line 1351
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2333 line 1353
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2334 line 1388
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2334 line 1394
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2334 line 1396
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2335 line 1431
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2335 line 1437
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2335 line 1439
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2336 line 1474
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2336 line 1480
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2336 line 1482
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2337 line 1517
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2337 line 1523
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2337 line 1525
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2338 line 1560
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2338 line 1566
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2338 line 1568
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2339 line 1603
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2339 line 1609
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2339 line 1611
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2340 line 1646
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2340 line 1652
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2340 line 1654
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2341 line 1689
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2341 line 1695
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2341 line 1697
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2342 line 1732
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2342 line 1738
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2342 line 1740
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2343 line 1775
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2343 line 1781
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2343 line 1783
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2344 line 1818
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2344 line 1824
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2344 line 1826
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2345 line 1861
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2345 line 1867
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2345 line 1869
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2346 line 1904
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2346 line 1910
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2346 line 1912
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2347 line 1947
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2347 line 1953
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2347 line 1955
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2348 line 1990
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2348 line 1996
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2348 line 1998
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2349 line 2033
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2349 line 2039
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2349 line 2041
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2350 line 2076
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2350 line 2082
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2350 line 2084
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2351 line 2119
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2351 line 2125
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2351 line 2127
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2352 line 2162
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2352 line 2168
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2352 line 2170
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2353 line 2205
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2353 line 2211
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2353 line 2213
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2354 line 2248
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2354 line 2254
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2354 line 2256
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2355 line 2291
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2355 line 2297
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2355 line 2299
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2356 line 2334
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2356 line 2340
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2356 line 2342
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2357 line 2377
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2357 line 2383
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2357 line 2385
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2358 line 2420
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2358 line 2426
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2358 line 2428
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2359 line 2463
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2359 line 2469
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2359 line 2471
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2360 line 2506
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2360 line 2512
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2360 line 2514
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2361 line 2549
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2361 line 2555
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2361 line 2557
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2362 line 2592
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2362 line 2598
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2362 line 2600
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2363 line 2635
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2363 line 2641
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2363 line 2643
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2364 line 2678
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2364 line 2684
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2364 line 2686
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2365 line 2721
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2365 line 2727
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2365 line 2729
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2366 line 2764
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2366 line 2770
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2366 line 2772
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2367 line 2807
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2367 line 2813
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2367 line 2815