OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound50.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3200 line 98
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3200 line 104
3. theorem OAI.MUB6.Certificate.PairSemantics.sound3200 line 106
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3201 line 146
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3201 line 152
6. theorem OAI.MUB6.Certificate.PairSemantics.sound3201 line 154
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3202 line 194
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3202 line 200
9. theorem OAI.MUB6.Certificate.PairSemantics.sound3202 line 202
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3203 line 242
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3203 line 248
12. theorem OAI.MUB6.Certificate.PairSemantics.sound3203 line 250
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3204 line 290
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3204 line 296
15. theorem OAI.MUB6.Certificate.PairSemantics.sound3204 line 298
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3205 line 338
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3205 line 344
18. theorem OAI.MUB6.Certificate.PairSemantics.sound3205 line 346
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3206 line 386
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3206 line 392
21. theorem OAI.MUB6.Certificate.PairSemantics.sound3206 line 394
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3207 line 434
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3207 line 440
24. theorem OAI.MUB6.Certificate.PairSemantics.sound3207 line 442
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3208 line 482
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3208 line 488
27. theorem OAI.MUB6.Certificate.PairSemantics.sound3208 line 490
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3209 line 530
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3209 line 536
30. theorem OAI.MUB6.Certificate.PairSemantics.sound3209 line 538
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3210 line 578
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3210 line 584
33. theorem OAI.MUB6.Certificate.PairSemantics.sound3210 line 586
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3211 line 626
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3211 line 632
36. theorem OAI.MUB6.Certificate.PairSemantics.sound3211 line 634
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3212 line 674
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3212 line 680
39. theorem OAI.MUB6.Certificate.PairSemantics.sound3212 line 682
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3213 line 722
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3213 line 728
42. theorem OAI.MUB6.Certificate.PairSemantics.sound3213 line 730
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3214 line 770
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3214 line 776
45. theorem OAI.MUB6.Certificate.PairSemantics.sound3214 line 778
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3215 line 818
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3215 line 824
48. theorem OAI.MUB6.Certificate.PairSemantics.sound3215 line 826
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3216 line 866
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3216 line 872
51. theorem OAI.MUB6.Certificate.PairSemantics.sound3216 line 874
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3217 line 914
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3217 line 920
54. theorem OAI.MUB6.Certificate.PairSemantics.sound3217 line 922
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3218 line 962
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3218 line 968
57. theorem OAI.MUB6.Certificate.PairSemantics.sound3218 line 970
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3219 line 1010
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3219 line 1016
60. theorem OAI.MUB6.Certificate.PairSemantics.sound3219 line 1018
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3220 line 1058
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3220 line 1064
63. theorem OAI.MUB6.Certificate.PairSemantics.sound3220 line 1066
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3221 line 1106
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3221 line 1112
66. theorem OAI.MUB6.Certificate.PairSemantics.sound3221 line 1114
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3222 line 1154
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3222 line 1160
69. theorem OAI.MUB6.Certificate.PairSemantics.sound3222 line 1162
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3223 line 1202
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3223 line 1208
72. theorem OAI.MUB6.Certificate.PairSemantics.sound3223 line 1210
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3224 line 1250
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3224 line 1256
75. theorem OAI.MUB6.Certificate.PairSemantics.sound3224 line 1258
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3225 line 1298
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3225 line 1304
78. theorem OAI.MUB6.Certificate.PairSemantics.sound3225 line 1306
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3226 line 1346
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3226 line 1352
81. theorem OAI.MUB6.Certificate.PairSemantics.sound3226 line 1354
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3227 line 1394
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3227 line 1400
84. theorem OAI.MUB6.Certificate.PairSemantics.sound3227 line 1402
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3228 line 1442
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3228 line 1448
87. theorem OAI.MUB6.Certificate.PairSemantics.sound3228 line 1450
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3229 line 1490
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3229 line 1496
90. theorem OAI.MUB6.Certificate.PairSemantics.sound3229 line 1498
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3230 line 1538
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3230 line 1544
93. theorem OAI.MUB6.Certificate.PairSemantics.sound3230 line 1546
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3231 line 1586
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3231 line 1592
96. theorem OAI.MUB6.Certificate.PairSemantics.sound3231 line 1594
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3232 line 1634
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3232 line 1640
99. theorem OAI.MUB6.Certificate.PairSemantics.sound3232 line 1642
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3233 line 1682
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3233 line 1688
102. theorem OAI.MUB6.Certificate.PairSemantics.sound3233 line 1690
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3234 line 1730
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3234 line 1736
105. theorem OAI.MUB6.Certificate.PairSemantics.sound3234 line 1738
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3235 line 1778
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3235 line 1784
108. theorem OAI.MUB6.Certificate.PairSemantics.sound3235 line 1786
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3236 line 1826
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3236 line 1832
111. theorem OAI.MUB6.Certificate.PairSemantics.sound3236 line 1834
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3237 line 1874
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3237 line 1880
114. theorem OAI.MUB6.Certificate.PairSemantics.sound3237 line 1882
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3238 line 1922
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3238 line 1928
117. theorem OAI.MUB6.Certificate.PairSemantics.sound3238 line 1930
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3239 line 1970
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3239 line 1976
120. theorem OAI.MUB6.Certificate.PairSemantics.sound3239 line 1978
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3240 line 2018
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3240 line 2024
123. theorem OAI.MUB6.Certificate.PairSemantics.sound3240 line 2026
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3241 line 2066
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3241 line 2072
126. theorem OAI.MUB6.Certificate.PairSemantics.sound3241 line 2074
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3242 line 2114
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3242 line 2120
129. theorem OAI.MUB6.Certificate.PairSemantics.sound3242 line 2122
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3243 line 2162
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3243 line 2168
132. theorem OAI.MUB6.Certificate.PairSemantics.sound3243 line 2170
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3244 line 2210
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3244 line 2216
135. theorem OAI.MUB6.Certificate.PairSemantics.sound3244 line 2218
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3245 line 2258
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3245 line 2264
138. theorem OAI.MUB6.Certificate.PairSemantics.sound3245 line 2266
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3246 line 2306
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3246 line 2312
141. theorem OAI.MUB6.Certificate.PairSemantics.sound3246 line 2314
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3247 line 2354
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3247 line 2360
144. theorem OAI.MUB6.Certificate.PairSemantics.sound3247 line 2362
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3248 line 2402
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3248 line 2408
147. theorem OAI.MUB6.Certificate.PairSemantics.sound3248 line 2410
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3249 line 2450
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3249 line 2456
150. theorem OAI.MUB6.Certificate.PairSemantics.sound3249 line 2458
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3250 line 2498
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3250 line 2504
153. theorem OAI.MUB6.Certificate.PairSemantics.sound3250 line 2506
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3251 line 2546
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3251 line 2552
156. theorem OAI.MUB6.Certificate.PairSemantics.sound3251 line 2554
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3252 line 2594
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3252 line 2600
159. theorem OAI.MUB6.Certificate.PairSemantics.sound3252 line 2602
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3253 line 2642
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3253 line 2648
162. theorem OAI.MUB6.Certificate.PairSemantics.sound3253 line 2650
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3254 line 2690
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3254 line 2696
165. theorem OAI.MUB6.Certificate.PairSemantics.sound3254 line 2698
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3255 line 2738
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3255 line 2744
168. theorem OAI.MUB6.Certificate.PairSemantics.sound3255 line 2746
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3256 line 2786
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3256 line 2792
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3256 line 2794
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3257 line 2834
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3257 line 2840
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3257 line 2842
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3258 line 2882
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3258 line 2888
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3258 line 2890
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3259 line 2930
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3259 line 2936
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3259 line 2938
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3260 line 2978
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3260 line 2984
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3260 line 2986
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3261 line 3026
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3261 line 3032
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3261 line 3034
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3262 line 3074
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3262 line 3080
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3262 line 3082
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3263 line 3122
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3263 line 3128
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3263 line 3130