OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound51.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3264 line 99
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3264 line 105
3. theorem OAI.MUB6.Certificate.PairSemantics.sound3264 line 107
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3265 line 147
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3265 line 153
6. theorem OAI.MUB6.Certificate.PairSemantics.sound3265 line 155
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3266 line 195
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3266 line 201
9. theorem OAI.MUB6.Certificate.PairSemantics.sound3266 line 203
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3267 line 243
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3267 line 249
12. theorem OAI.MUB6.Certificate.PairSemantics.sound3267 line 251
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3268 line 291
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3268 line 297
15. theorem OAI.MUB6.Certificate.PairSemantics.sound3268 line 299
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3269 line 339
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3269 line 345
18. theorem OAI.MUB6.Certificate.PairSemantics.sound3269 line 347
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3270 line 387
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3270 line 393
21. theorem OAI.MUB6.Certificate.PairSemantics.sound3270 line 395
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3271 line 435
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3271 line 441
24. theorem OAI.MUB6.Certificate.PairSemantics.sound3271 line 443
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3272 line 483
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3272 line 489
27. theorem OAI.MUB6.Certificate.PairSemantics.sound3272 line 491
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3273 line 531
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3273 line 537
30. theorem OAI.MUB6.Certificate.PairSemantics.sound3273 line 539
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3274 line 579
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3274 line 585
33. theorem OAI.MUB6.Certificate.PairSemantics.sound3274 line 587
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3275 line 627
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3275 line 633
36. theorem OAI.MUB6.Certificate.PairSemantics.sound3275 line 635
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3276 line 675
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3276 line 681
39. theorem OAI.MUB6.Certificate.PairSemantics.sound3276 line 683
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3277 line 723
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3277 line 729
42. theorem OAI.MUB6.Certificate.PairSemantics.sound3277 line 731
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3278 line 771
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3278 line 777
45. theorem OAI.MUB6.Certificate.PairSemantics.sound3278 line 779
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3279 line 819
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3279 line 825
48. theorem OAI.MUB6.Certificate.PairSemantics.sound3279 line 827
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3280 line 867
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3280 line 873
51. theorem OAI.MUB6.Certificate.PairSemantics.sound3280 line 875
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3281 line 915
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3281 line 921
54. theorem OAI.MUB6.Certificate.PairSemantics.sound3281 line 923
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3282 line 963
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3282 line 969
57. theorem OAI.MUB6.Certificate.PairSemantics.sound3282 line 971
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3283 line 1011
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3283 line 1017
60. theorem OAI.MUB6.Certificate.PairSemantics.sound3283 line 1019
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3284 line 1059
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3284 line 1065
63. theorem OAI.MUB6.Certificate.PairSemantics.sound3284 line 1067
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3285 line 1107
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3285 line 1113
66. theorem OAI.MUB6.Certificate.PairSemantics.sound3285 line 1115
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3286 line 1155
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3286 line 1161
69. theorem OAI.MUB6.Certificate.PairSemantics.sound3286 line 1163
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3287 line 1203
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3287 line 1209
72. theorem OAI.MUB6.Certificate.PairSemantics.sound3287 line 1211
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3288 line 1251
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3288 line 1257
75. theorem OAI.MUB6.Certificate.PairSemantics.sound3288 line 1259
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3289 line 1299
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3289 line 1305
78. theorem OAI.MUB6.Certificate.PairSemantics.sound3289 line 1307
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3290 line 1347
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3290 line 1353
81. theorem OAI.MUB6.Certificate.PairSemantics.sound3290 line 1355
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3291 line 1395
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3291 line 1401
84. theorem OAI.MUB6.Certificate.PairSemantics.sound3291 line 1403
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3292 line 1443
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3292 line 1449
87. theorem OAI.MUB6.Certificate.PairSemantics.sound3292 line 1451
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3293 line 1491
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3293 line 1497
90. theorem OAI.MUB6.Certificate.PairSemantics.sound3293 line 1499
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3294 line 1539
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3294 line 1545
93. theorem OAI.MUB6.Certificate.PairSemantics.sound3294 line 1547
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3295 line 1587
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3295 line 1593
96. theorem OAI.MUB6.Certificate.PairSemantics.sound3295 line 1595
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3296 line 1635
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3296 line 1641
99. theorem OAI.MUB6.Certificate.PairSemantics.sound3296 line 1643
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3297 line 1683
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3297 line 1689
102. theorem OAI.MUB6.Certificate.PairSemantics.sound3297 line 1691
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3298 line 1731
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3298 line 1737
105. theorem OAI.MUB6.Certificate.PairSemantics.sound3298 line 1739
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3299 line 1779
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3299 line 1785
108. theorem OAI.MUB6.Certificate.PairSemantics.sound3299 line 1787
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3300 line 1827
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3300 line 1833
111. theorem OAI.MUB6.Certificate.PairSemantics.sound3300 line 1835
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3301 line 1875
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3301 line 1881
114. theorem OAI.MUB6.Certificate.PairSemantics.sound3301 line 1883
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3302 line 1923
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3302 line 1929
117. theorem OAI.MUB6.Certificate.PairSemantics.sound3302 line 1931
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3303 line 1971
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3303 line 1977
120. theorem OAI.MUB6.Certificate.PairSemantics.sound3303 line 1979
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3304 line 2019
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3304 line 2025
123. theorem OAI.MUB6.Certificate.PairSemantics.sound3304 line 2027
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3305 line 2067
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3305 line 2073
126. theorem OAI.MUB6.Certificate.PairSemantics.sound3305 line 2075
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3306 line 2115
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3306 line 2121
129. theorem OAI.MUB6.Certificate.PairSemantics.sound3306 line 2123
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3307 line 2163
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3307 line 2169
132. theorem OAI.MUB6.Certificate.PairSemantics.sound3307 line 2171
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3308 line 2211
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3308 line 2217
135. theorem OAI.MUB6.Certificate.PairSemantics.sound3308 line 2219
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3309 line 2259
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3309 line 2265
138. theorem OAI.MUB6.Certificate.PairSemantics.sound3309 line 2267
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3310 line 2307
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3310 line 2313
141. theorem OAI.MUB6.Certificate.PairSemantics.sound3310 line 2315
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3311 line 2355
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3311 line 2361
144. theorem OAI.MUB6.Certificate.PairSemantics.sound3311 line 2363
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3312 line 2403
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3312 line 2409
147. theorem OAI.MUB6.Certificate.PairSemantics.sound3312 line 2411
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3313 line 2451
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3313 line 2457
150. theorem OAI.MUB6.Certificate.PairSemantics.sound3313 line 2459
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3314 line 2499
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3314 line 2505
153. theorem OAI.MUB6.Certificate.PairSemantics.sound3314 line 2507
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3315 line 2547
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3315 line 2553
156. theorem OAI.MUB6.Certificate.PairSemantics.sound3315 line 2555
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3316 line 2595
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3316 line 2601
159. theorem OAI.MUB6.Certificate.PairSemantics.sound3316 line 2603
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3317 line 2643
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3317 line 2649
162. theorem OAI.MUB6.Certificate.PairSemantics.sound3317 line 2651
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3318 line 2691
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3318 line 2697
165. theorem OAI.MUB6.Certificate.PairSemantics.sound3318 line 2699
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3319 line 2739
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3319 line 2745
168. theorem OAI.MUB6.Certificate.PairSemantics.sound3319 line 2747
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3320 line 2787
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3320 line 2793
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3320 line 2795
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3321 line 2835
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3321 line 2841
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3321 line 2843
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3322 line 2883
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3322 line 2889
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3322 line 2891
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3323 line 2931
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3323 line 2937
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3323 line 2939
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3324 line 2979
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3324 line 2985
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3324 line 2987
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3325 line 3027
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3325 line 3033
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3325 line 3035
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3326 line 3075
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3326 line 3081
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3326 line 3083
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3327 line 3123
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3327 line 3129
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3327 line 3131