OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound52.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3328 line 97
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3328 line 103
3. theorem OAI.MUB6.Certificate.PairSemantics.sound3328 line 105
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3329 line 145
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3329 line 151
6. theorem OAI.MUB6.Certificate.PairSemantics.sound3329 line 153
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3330 line 193
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3330 line 199
9. theorem OAI.MUB6.Certificate.PairSemantics.sound3330 line 201
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3331 line 241
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3331 line 247
12. theorem OAI.MUB6.Certificate.PairSemantics.sound3331 line 249
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3332 line 289
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3332 line 295
15. theorem OAI.MUB6.Certificate.PairSemantics.sound3332 line 297
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3333 line 337
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3333 line 343
18. theorem OAI.MUB6.Certificate.PairSemantics.sound3333 line 345
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3334 line 385
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3334 line 391
21. theorem OAI.MUB6.Certificate.PairSemantics.sound3334 line 393
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3335 line 433
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3335 line 439
24. theorem OAI.MUB6.Certificate.PairSemantics.sound3335 line 441
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3336 line 481
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3336 line 487
27. theorem OAI.MUB6.Certificate.PairSemantics.sound3336 line 489
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3337 line 529
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3337 line 535
30. theorem OAI.MUB6.Certificate.PairSemantics.sound3337 line 537
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3338 line 577
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3338 line 583
33. theorem OAI.MUB6.Certificate.PairSemantics.sound3338 line 585
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3339 line 625
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3339 line 631
36. theorem OAI.MUB6.Certificate.PairSemantics.sound3339 line 633
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3340 line 673
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3340 line 679
39. theorem OAI.MUB6.Certificate.PairSemantics.sound3340 line 681
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3341 line 721
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3341 line 727
42. theorem OAI.MUB6.Certificate.PairSemantics.sound3341 line 729
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3342 line 769
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3342 line 775
45. theorem OAI.MUB6.Certificate.PairSemantics.sound3342 line 777
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3343 line 817
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3343 line 823
48. theorem OAI.MUB6.Certificate.PairSemantics.sound3343 line 825
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3344 line 865
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3344 line 871
51. theorem OAI.MUB6.Certificate.PairSemantics.sound3344 line 873
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3345 line 913
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3345 line 919
54. theorem OAI.MUB6.Certificate.PairSemantics.sound3345 line 921
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3346 line 961
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3346 line 967
57. theorem OAI.MUB6.Certificate.PairSemantics.sound3346 line 969
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3347 line 1009
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3347 line 1015
60. theorem OAI.MUB6.Certificate.PairSemantics.sound3347 line 1017
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3348 line 1057
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3348 line 1063
63. theorem OAI.MUB6.Certificate.PairSemantics.sound3348 line 1065
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3349 line 1105
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3349 line 1111
66. theorem OAI.MUB6.Certificate.PairSemantics.sound3349 line 1113
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3350 line 1153
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3350 line 1159
69. theorem OAI.MUB6.Certificate.PairSemantics.sound3350 line 1161
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3351 line 1201
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3351 line 1207
72. theorem OAI.MUB6.Certificate.PairSemantics.sound3351 line 1209
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3352 line 1249
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3352 line 1255
75. theorem OAI.MUB6.Certificate.PairSemantics.sound3352 line 1257
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3353 line 1297
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3353 line 1303
78. theorem OAI.MUB6.Certificate.PairSemantics.sound3353 line 1305
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3354 line 1345
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3354 line 1351
81. theorem OAI.MUB6.Certificate.PairSemantics.sound3354 line 1353
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3355 line 1393
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3355 line 1399
84. theorem OAI.MUB6.Certificate.PairSemantics.sound3355 line 1401
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3356 line 1441
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3356 line 1447
87. theorem OAI.MUB6.Certificate.PairSemantics.sound3356 line 1449
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3357 line 1489
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3357 line 1495
90. theorem OAI.MUB6.Certificate.PairSemantics.sound3357 line 1497
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3358 line 1537
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3358 line 1543
93. theorem OAI.MUB6.Certificate.PairSemantics.sound3358 line 1545
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3359 line 1585
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3359 line 1591
96. theorem OAI.MUB6.Certificate.PairSemantics.sound3359 line 1593
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3360 line 1633
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3360 line 1639
99. theorem OAI.MUB6.Certificate.PairSemantics.sound3360 line 1641
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3361 line 1681
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3361 line 1687
102. theorem OAI.MUB6.Certificate.PairSemantics.sound3361 line 1689
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3362 line 1729
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3362 line 1735
105. theorem OAI.MUB6.Certificate.PairSemantics.sound3362 line 1737
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3363 line 1777
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3363 line 1783
108. theorem OAI.MUB6.Certificate.PairSemantics.sound3363 line 1785
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3364 line 1825
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3364 line 1831
111. theorem OAI.MUB6.Certificate.PairSemantics.sound3364 line 1833
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3365 line 1873
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3365 line 1879
114. theorem OAI.MUB6.Certificate.PairSemantics.sound3365 line 1881
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3366 line 1921
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3366 line 1927
117. theorem OAI.MUB6.Certificate.PairSemantics.sound3366 line 1929
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3367 line 1969
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3367 line 1975
120. theorem OAI.MUB6.Certificate.PairSemantics.sound3367 line 1977
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3368 line 2017
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3368 line 2023
123. theorem OAI.MUB6.Certificate.PairSemantics.sound3368 line 2025
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3369 line 2065
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3369 line 2071
126. theorem OAI.MUB6.Certificate.PairSemantics.sound3369 line 2073
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3370 line 2113
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3370 line 2119
129. theorem OAI.MUB6.Certificate.PairSemantics.sound3370 line 2121
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3371 line 2161
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3371 line 2167
132. theorem OAI.MUB6.Certificate.PairSemantics.sound3371 line 2169
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3372 line 2209
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3372 line 2215
135. theorem OAI.MUB6.Certificate.PairSemantics.sound3372 line 2217
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3373 line 2257
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3373 line 2263
138. theorem OAI.MUB6.Certificate.PairSemantics.sound3373 line 2265
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3374 line 2305
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3374 line 2311
141. theorem OAI.MUB6.Certificate.PairSemantics.sound3374 line 2313
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3375 line 2353
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3375 line 2359
144. theorem OAI.MUB6.Certificate.PairSemantics.sound3375 line 2361
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3376 line 2401
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3376 line 2407
147. theorem OAI.MUB6.Certificate.PairSemantics.sound3376 line 2409
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3377 line 2449
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3377 line 2455
150. theorem OAI.MUB6.Certificate.PairSemantics.sound3377 line 2457
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3378 line 2497
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3378 line 2503
153. theorem OAI.MUB6.Certificate.PairSemantics.sound3378 line 2505
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3379 line 2545
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3379 line 2551
156. theorem OAI.MUB6.Certificate.PairSemantics.sound3379 line 2553
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3380 line 2593
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3380 line 2599
159. theorem OAI.MUB6.Certificate.PairSemantics.sound3380 line 2601
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3381 line 2641
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3381 line 2647
162. theorem OAI.MUB6.Certificate.PairSemantics.sound3381 line 2649
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3382 line 2689
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3382 line 2695
165. theorem OAI.MUB6.Certificate.PairSemantics.sound3382 line 2697
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3383 line 2737
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3383 line 2743
168. theorem OAI.MUB6.Certificate.PairSemantics.sound3383 line 2745
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3384 line 2785
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3384 line 2791
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3384 line 2793
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3385 line 2833
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3385 line 2839
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3385 line 2841
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3386 line 2881
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3386 line 2887
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3386 line 2889
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3387 line 2929
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3387 line 2935
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3387 line 2937
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3388 line 2977
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3388 line 2983
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3388 line 2985
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3389 line 3025
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3389 line 3031
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3389 line 3033
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3390 line 3073
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3390 line 3079
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3390 line 3081
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3391 line 3121
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3391 line 3127
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3391 line 3129